src/HOL/MicroJava/DFA/Opt.thy
changeset 58860 fee7cfa69c50
parent 55466 786edc984c98
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/DFA/Opt.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Opt.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4  done 
     1.5  
     1.6  lemma le_None [iff]:
     1.7 -  "(ox <=_(le r) None) = (ox = None)";
     1.8 +  "(ox <=_(le r) None) = (ox = None)"
     1.9  apply (unfold lesub_def le_def)
    1.10  apply (simp split: option.split)
    1.11  done 
    1.12 @@ -282,7 +282,7 @@
    1.13  
    1.14  lemma option_map_in_optionI:
    1.15    "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
    1.16 -  \<Longrightarrow> map_option f ox : opt S";
    1.17 +  \<Longrightarrow> map_option f ox : opt S"
    1.18  apply (unfold map_option_case)
    1.19  apply (simp split: option.split)
    1.20  apply blast