src/HOL/MicroJava/DFA/Product.thy
changeset 58860 fee7cfa69c50
parent 53015 a1119cf551e8
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/DFA/Product.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Product.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5  lemma closed_lift2_sup:
     1.6    "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
     1.7 -  closed (err(A<*>B)) (lift2(sup f g))";
     1.8 +  closed (err(A<*>B)) (lift2(sup f g))"
     1.9  apply (unfold closed_def plussub_def lift2_def err_def sup_def)
    1.10  apply (simp split: err.split)
    1.11  apply blast