src/HOL/MicroJava/DFA/Err.thy

 apply simp
 apply fast
 done 
 
 text \<open>
-  If @{term "AS = {}"} the thm collapses to
-  @{prop "order r & closed {Err} f & Err +_f Err = Err"}
+  If \<^term>\<open>AS = {}\<close> the thm collapses to
+  \<^prop>\<open>order r & closed {Err} f & Err +_f Err = Err\<close>
   which may not hold 
 \<close>
 lemma err_semilat_UnionI:
   "\<lbrakk> \<forall>A\<in>AS. err_semilat(A, r, f); AS \<noteq> {}; 
       \<forall>A\<in>AS. \<forall>B\<in>AS. A\<noteq>B \<longrightarrow> (\<forall>a\<in>A. \<forall>b\<in>B. \<not> a <=_r b & a +_f b = Err) \<rbrakk>