src/ZF/AC/HH.thy

 definition
   HH :: "[i, i, i] => i"  where
     "HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c \<in> b. r`c)
                                     in  if f`z \<in> Pow(z)-{0} then f`z else {x})"
 
-subsection{*Lemmas useful in each of the three proofs*}
+subsection\<open>Lemmas useful in each of the three proofs\<close>
 
 lemma HH_def_satisfies_eq:
      "HH(f,x,a) = (let z = x - (\<Union>b \<in> a. HH(f,x,b))   
                    in  if f`z \<in> Pow(z)-{0} then f`z else {x})"
 by (rule HH_def [THEN def_transrec, THEN trans], simp)

 apply (rule HH_values [THEN disjE], assumption)
 apply (rule less_LeastE)
 apply (erule_tac [2] ltI [OF _ Ord_Least], assumption)
 done
 
-subsection{*Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1*}
+subsection\<open>Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1\<close>
 
 lemma lam_Least_HH_inj_Pow: 
         "(\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))   
          \<in> inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"
 apply (unfold inj_def, simp)

 lemmas bij_Least_HH_x =  
     comp_bij [OF f_sing_lam_bij [OF _ lam_singI] 
               lam_sing_bij [THEN bij_converse_bij]]
 
 
-subsection{*The proof of AC1 ==> WO2*}
+subsection\<open>The proof of AC1 ==> WO2\<close>
 
 (*Establishing the existence of a bijection, namely
 converse
  (converse(\<lambda>x\<in>x. {x}) O
   Lambda