src/HOL/MicroJava/DFA/Err.thy
changeset 58860 fee7cfa69c50
parent 58310 91ea607a34d8
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/DFA/Err.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Err.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4   "OK x <=_(le r) e  =  (e = Err | (? y. e = OK y & x <=_r y))"
     1.5    by (simp add: unfold_lesub_err le_def split: err.split)
     1.6  
     1.7 -lemma top_Err [iff]: "top (le r) Err";
     1.8 +lemma top_Err [iff]: "top (le r) Err"
     1.9    by (simp add: top_def)
    1.10  
    1.11  lemma OK_less_conv [rule_format, iff]:
    1.12 @@ -231,7 +231,7 @@
    1.13  
    1.14  lemma semilat_le_err_OK1:
    1.15    "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
    1.16 -  \<Longrightarrow> x <=_r z";
    1.17 +  \<Longrightarrow> x <=_r z"
    1.18  apply (rule OK_le_err_OK [THEN iffD1])
    1.19  apply (erule subst)
    1.20  apply (simp add: Semilat.ub1 [OF Semilat.intro])