src/HOL/MicroJava/DFA/Err.thy

   apply (erule subst)
   apply (blast intro: Semilat.closedI [OF Semilat.intro] closedD)
   done 
 qed
 
-subsection \<open>semilat (err(Union AS))\<close>
+subsection \<open>semilat (err (Union AS))\<close>
 
 (* FIXME? *)
 lemma all_bex_swap_lemma [iff]:
   "(!x. (? y:A. x = f y) \<longrightarrow> P x) = (!y:A. P(f y))"
   by blast
 
 lemma closed_err_Union_lift2I: 
   "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {}; 
       !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk> 
-  \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
+  \<Longrightarrow> closed (err (\<Union>AS)) (lift2 f)"
 apply (unfold closed_def err_def)
 apply simp
 apply clarify
 apply simp
 apply fast

   which may not hold 
 \<close>
 lemma err_semilat_UnionI:
   "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
       !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
-  \<Longrightarrow> err_semilat(Union AS, r, f)"
+  \<Longrightarrow> err_semilat (\<Union>AS, r, f)"
 apply (unfold semilat_def sl_def)
 apply (simp add: closed_err_Union_lift2I)
 apply (rule conjI)
  apply blast
 apply (simp add: err_def)