src/ZF/Constructible/Normal.thy

       c.u.\<close>
 
 text\<open>The constructions below come from Kunen, \emph{Set Theory}, page 78.\<close>
 locale cub_family =
   fixes P and A
-  fixes next_greater \<comment> "the next ordinal satisfying class @{term A}"
-  fixes sup_greater  \<comment> "sup of those ordinals over all @{term A}"
+  fixes next_greater \<comment> \<open>the next ordinal satisfying class @{term A}\<close>
+  fixes sup_greater  \<comment> \<open>sup of those ordinals over all @{term A}\<close>
   assumes closed:    "a\<in>A ==> Closed(P(a))"
       and unbounded: "a\<in>A ==> Unbounded(P(a))"
       and A_non0: "A\<noteq>0"
   defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)"
       and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"

 lemma iterates_omega_Limit:
      "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"  
 apply (frule lt_Ord) 
 apply (simp add: iterates_omega_def)
 apply (rule increasing_LimitI) 
-   \<comment>"this lemma is @{thm increasing_LimitI [no_vars]}"
+   \<comment> \<open>this lemma is @{thm increasing_LimitI [no_vars]}\<close>
  apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
                      Ord_UN Ord_iterates lt_imp_0_lt
                      iterates_Normal_increasing, clarify)
 apply (rule bexI) 
  apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal])