isabelle update_cartouches -c -t;
authorwenzelm
Mon Dec 07 10:23:50 2015 +0100 (2015-12-07)
changeset 6179827f3c10b0b50
parent 61797 458b4e3720ab
child 61799 4cf66f21b764
isabelle update_cartouches -c -t;
src/ZF/AC/AC_Equiv.thy
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/Bin.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Rank.thy
src/ZF/Constructible/Rank_Separation.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/EquivClass.thy
src/ZF/IMP/Equiv.thy
src/ZF/Induct/Acc.thy
src/ZF/Induct/Binary_Trees.thy
src/ZF/Induct/Brouwer.thy
src/ZF/Induct/Comb.thy
src/ZF/Induct/Datatypes.thy
src/ZF/Induct/ListN.thy
src/ZF/Induct/Multiset.thy
src/ZF/Induct/Ntree.thy
src/ZF/Induct/Primrec.thy
src/ZF/Induct/PropLog.thy
src/ZF/Induct/Rmap.thy
src/ZF/Induct/Term.thy
src/ZF/Induct/Tree_Forest.thy
src/ZF/InfDatatype.thy
src/ZF/IntDiv_ZF.thy
src/ZF/Int_ZF.thy
src/ZF/List_ZF.thy
src/ZF/Order.thy
src/ZF/OrderArith.thy
src/ZF/Ordinal.thy
src/ZF/UNITY/AllocBase.thy
src/ZF/UNITY/Distributor.thy
src/ZF/UNITY/Merge.thy
src/ZF/UNITY/Mutex.thy
src/ZF/UNITY/UNITY.thy
src/ZF/UNITY/WFair.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.thy
src/ZF/Zorn.thy
src/ZF/equalities.thy
src/ZF/ex/CoUnit.thy
src/ZF/ex/Group.thy
src/ZF/ex/Limit.thy
src/ZF/ex/Primes.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/misc.thy
src/ZF/upair.thy
     1.1 --- a/src/ZF/AC/AC_Equiv.thy	Mon Dec 07 10:19:30 2015 +0100
     1.2 +++ b/src/ZF/AC/AC_Equiv.thy	Mon Dec 07 10:23:50 2015 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4    assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
     1.5      ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
     1.6        (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
     1.7 -  --"AC18 cannot be expressed within the object-logic"
     1.8 +  \<comment>"AC18 cannot be expressed within the object-logic"
     1.9  
    1.10  definition
    1.11      "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
     2.1 --- a/src/ZF/Arith.thy	Mon Dec 07 10:19:30 2015 +0100
     2.2 +++ b/src/ZF/Arith.thy	Mon Dec 07 10:23:50 2015 +0100
     2.3 @@ -85,7 +85,7 @@
     2.4  lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
     2.5  
     2.6  
     2.7 -subsection\<open>@{text natify}, the Coercion to @{term nat}\<close>
     2.8 +subsection\<open>\<open>natify\<close>, the Coercion to @{term nat}\<close>
     2.9  
    2.10  lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
    2.11  by (unfold pred_def, auto)
    2.12 @@ -324,7 +324,7 @@
    2.13  lemma add_lt_mono2: "[| i<j; j\<in>nat |] ==> k#+i < k#+j"
    2.14  by (simp add: add_commute [of k] add_lt_mono1)
    2.15  
    2.16 -text\<open>A [clumsy] way of lifting < monotonicity to @{text "\<le>"} monotonicity\<close>
    2.17 +text\<open>A [clumsy] way of lifting < monotonicity to \<open>\<le>\<close> monotonicity\<close>
    2.18  lemma Ord_lt_mono_imp_le_mono:
    2.19    assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
    2.20        and ford:    "!!i. i:k ==> Ord(f(i))"
    2.21 @@ -335,13 +335,13 @@
    2.22  apply (blast intro!: leCI lt_mono ford elim!: leE)
    2.23  done
    2.24  
    2.25 -text\<open>@{text "\<le>"} monotonicity, 1st argument\<close>
    2.26 +text\<open>\<open>\<le>\<close> monotonicity, 1st argument\<close>
    2.27  lemma add_le_mono1: "[| i \<le> j; j\<in>nat |] ==> i#+k \<le> j#+k"
    2.28  apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
    2.29  apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
    2.30  done
    2.31  
    2.32 -text\<open>@{text "\<le>"} monotonicity, both arguments\<close>
    2.33 +text\<open>\<open>\<le>\<close> monotonicity, both arguments\<close>
    2.34  lemma add_le_mono: "[| i \<le> j; k \<le> l; j\<in>nat; l\<in>nat |] ==> i#+k \<le> j#+l"
    2.35  apply (rule add_le_mono1 [THEN le_trans], assumption+)
    2.36  apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
     3.1 --- a/src/ZF/ArithSimp.thy	Mon Dec 07 10:19:30 2015 +0100
     3.2 +++ b/src/ZF/ArithSimp.thy	Mon Dec 07 10:23:50 2015 +0100
     3.3 @@ -264,7 +264,7 @@
     3.4  by (cut_tac n = 0 in mod2_add_more, auto)
     3.5  
     3.6  
     3.7 -subsection\<open>Additional theorems about @{text "\<le>"}\<close>
     3.8 +subsection\<open>Additional theorems about \<open>\<le>\<close>\<close>
     3.9  
    3.10  lemma add_le_self: "m:nat ==> m \<le> (m #+ n)"
    3.11  apply (simp (no_asm_simp))
     4.1 --- a/src/ZF/Bin.thy	Mon Dec 07 10:19:30 2015 +0100
     4.2 +++ b/src/ZF/Bin.thy	Mon Dec 07 10:23:50 2015 +0100
     4.3 @@ -697,7 +697,7 @@
     4.4  
     4.5  subsection \<open>examples:\<close>
     4.6  
     4.7 -text \<open>@{text combine_numerals_prod} (products of separate literals)\<close>
     4.8 +text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
     4.9  lemma "#5 $* x $* #3 = y" apply simp oops
    4.10  
    4.11  schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops
     5.1 --- a/src/ZF/Cardinal.thy	Mon Dec 07 10:19:30 2015 +0100
     5.2 +++ b/src/ZF/Cardinal.thy	Mon Dec 07 10:23:50 2015 +0100
     5.3 @@ -439,10 +439,10 @@
     5.4  proof (unfold cardinal_def)
     5.5    show "Card(\<mu> i. i \<approx> A)"
     5.6      proof (cases "\<exists>i. Ord (i) & i \<approx> A")
     5.7 -      case False thus ?thesis           --\<open>degenerate case\<close>
     5.8 +      case False thus ?thesis           \<comment>\<open>degenerate case\<close>
     5.9          by (simp add: Least_0 Card_0)
    5.10      next
    5.11 -      case True                         --\<open>real case: @{term A} is isomorphic to some ordinal\<close>
    5.12 +      case True                         \<comment>\<open>real case: @{term A} is isomorphic to some ordinal\<close>
    5.13        then obtain i where i: "Ord(i)" "i \<approx> A" by blast
    5.14        show ?thesis
    5.15          proof (rule CardI [OF Ord_Least], rule notI)
    5.16 @@ -490,7 +490,7 @@
    5.17    thus ?thesis by simp
    5.18  qed
    5.19  
    5.20 -text\<open>Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of @{text cardinal_mono} fails!\<close>
    5.21 +text\<open>Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of \<open>cardinal_mono\<close> fails!\<close>
    5.22  lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
    5.23  apply (rule Ord_linear2 [of i j], assumption+)
    5.24  apply (erule lt_trans2 [THEN lt_irrefl])
    5.25 @@ -687,7 +687,7 @@
    5.26    thus ?thesis by auto
    5.27  qed
    5.28  
    5.29 -text\<open>A slightly weaker version of @{text nat_eqpoll_iff}\<close>
    5.30 +text\<open>A slightly weaker version of \<open>nat_eqpoll_iff\<close>\<close>
    5.31  lemma Ord_nat_eqpoll_iff:
    5.32    assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
    5.33  using i nat_into_Ord [OF n]
    5.34 @@ -1109,7 +1109,7 @@
    5.35  next
    5.36    case (succ x)
    5.37    hence wfx: "\<And>Z. Z = 0 \<or> (\<exists>z\<in>Z. \<forall>y. z \<in> y \<and> z \<in> x \<and> y \<in> x \<and> z \<in> x \<longrightarrow> y \<notin> Z)"
    5.38 -    by (simp add: wf_on_def wf_def)  --\<open>not easy to erase the duplicate @{term"z \<in> x"}!\<close>
    5.39 +    by (simp add: wf_on_def wf_def)  \<comment>\<open>not easy to erase the duplicate @{term"z \<in> x"}!\<close>
    5.40    show ?case
    5.41      proof (rule wf_onI)
    5.42        fix Z u
     6.1 --- a/src/ZF/CardinalArith.thy	Mon Dec 07 10:19:30 2015 +0100
     6.2 +++ b/src/ZF/CardinalArith.thy	Mon Dec 07 10:23:50 2015 +0100
     6.3 @@ -28,14 +28,14 @@
     6.4  
     6.5  definition
     6.6    jump_cardinal :: "i=>i"  where
     6.7 -    --\<open>This def is more complex than Kunen's but it more easily proved to
     6.8 +    \<comment>\<open>This def is more complex than Kunen's but it more easily proved to
     6.9          be a cardinal\<close>
    6.10      "jump_cardinal(K) ==
    6.11           \<Union>X\<in>Pow(K). {z. r \<in> Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    6.12  
    6.13  definition
    6.14    csucc         :: "i=>i"  where
    6.15 -    --\<open>needed because @{term "jump_cardinal(K)"} might not be the successor
    6.16 +    \<comment>\<open>needed because @{term "jump_cardinal(K)"} might not be the successor
    6.17          of @{term K}\<close>
    6.18      "csucc(K) == \<mu> L. Card(L) & K<L"
    6.19  
    6.20 @@ -574,7 +574,7 @@
    6.21    finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> |succ(z)| \<times> |succ(z)|" .
    6.22  qed
    6.23  
    6.24 -text\<open>Kunen: "... so the order type is @{text"\<le>"} K"\<close>
    6.25 +text\<open>Kunen: "... so the order type is \<open>\<le>\<close> K"\<close>
    6.26  lemma ordertype_csquare_le:
    6.27    assumes IK: "InfCard(K)" and eq: "\<And>y. y\<in>K \<Longrightarrow> InfCard(y) \<Longrightarrow> y \<otimes> y = y"
    6.28    shows "ordertype(K*K, csquare_rel(K)) \<le> K"
     7.1 --- a/src/ZF/Cardinal_AC.thy	Mon Dec 07 10:19:30 2015 +0100
     7.2 +++ b/src/ZF/Cardinal_AC.thy	Mon Dec 07 10:23:50 2015 +0100
     7.3 @@ -222,7 +222,7 @@
     7.4    note lt_subset_trans [OF _ _ OU, trans]
     7.5    show ?thesis
     7.6      proof (cases "W=0")
     7.7 -      case True  --\<open>solve the easy 0 case\<close>
     7.8 +      case True  \<comment>\<open>solve the easy 0 case\<close>
     7.9        thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
    7.10      next
    7.11        case False
     8.1 --- a/src/ZF/Constructible/AC_in_L.thy	Mon Dec 07 10:19:30 2015 +0100
     8.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Mon Dec 07 10:23:50 2015 +0100
     8.3 @@ -145,7 +145,7 @@
     8.4  nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k)
     8.5  enumerates the triangular numbers and can be defined by triangle(0)=0,
     8.6  triangle(succ(k)) = succ(k + triangle(k)).  Some small amount of effort is
     8.7 -needed to show that f is a bijection.  We already know that such a bijection exists by the theorem @{text well_ord_InfCard_square_eq}:
     8.8 +needed to show that f is a bijection.  We already know that such a bijection exists by the theorem \<open>well_ord_InfCard_square_eq\<close>:
     8.9  @{thm[display] well_ord_InfCard_square_eq[no_vars]}
    8.10  
    8.11  However, this result merely states that there is a bijection between the two
    8.12 @@ -233,20 +233,20 @@
    8.13  
    8.14  definition
    8.15    env_form_r :: "[i,i,i]=>i" where
    8.16 -    --\<open>wellordering on (environment, formula) pairs\<close>
    8.17 +    \<comment>\<open>wellordering on (environment, formula) pairs\<close>
    8.18     "env_form_r(f,r,A) ==
    8.19        rmult(list(A), rlist(A, r),
    8.20              formula, measure(formula, enum(f)))"
    8.21  
    8.22  definition
    8.23    env_form_map :: "[i,i,i,i]=>i" where
    8.24 -    --\<open>map from (environment, formula) pairs to ordinals\<close>
    8.25 +    \<comment>\<open>map from (environment, formula) pairs to ordinals\<close>
    8.26     "env_form_map(f,r,A,z)
    8.27        == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
    8.28  
    8.29  definition
    8.30    DPow_ord :: "[i,i,i,i,i]=>o" where
    8.31 -    --\<open>predicate that holds if @{term k} is a valid index for @{term X}\<close>
    8.32 +    \<comment>\<open>predicate that holds if @{term k} is a valid index for @{term X}\<close>
    8.33     "DPow_ord(f,r,A,X,k) ==
    8.34             \<exists>env \<in> list(A). \<exists>p \<in> formula.
    8.35               arity(p) \<le> succ(length(env)) &
    8.36 @@ -255,12 +255,12 @@
    8.37  
    8.38  definition
    8.39    DPow_least :: "[i,i,i,i]=>i" where
    8.40 -    --\<open>function yielding the smallest index for @{term X}\<close>
    8.41 +    \<comment>\<open>function yielding the smallest index for @{term X}\<close>
    8.42     "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
    8.43  
    8.44  definition
    8.45    DPow_r :: "[i,i,i]=>i" where
    8.46 -    --\<open>a wellordering on @{term "DPow(A)"}\<close>
    8.47 +    \<comment>\<open>a wellordering on @{term "DPow(A)"}\<close>
    8.48     "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))"
    8.49  
    8.50  
    8.51 @@ -332,7 +332,7 @@
    8.52  
    8.53  definition
    8.54    rlimit :: "[i,i=>i]=>i" where
    8.55 -  --\<open>Expresses the wellordering at limit ordinals.  The conditional
    8.56 +  \<comment>\<open>Expresses the wellordering at limit ordinals.  The conditional
    8.57        lets us remove the premise @{term "Limit(i)"} from some theorems.\<close>
    8.58      "rlimit(i,r) ==
    8.59         if Limit(i) then 
    8.60 @@ -344,7 +344,7 @@
    8.61  
    8.62  definition
    8.63    Lset_new :: "i=>i" where
    8.64 -  --\<open>This constant denotes the set of elements introduced at level
    8.65 +  \<comment>\<open>This constant denotes the set of elements introduced at level
    8.66        @{term "succ(i)"}\<close>
    8.67      "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
    8.68  
     9.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Mon Dec 07 10:19:30 2015 +0100
     9.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Mon Dec 07 10:23:50 2015 +0100
     9.3 @@ -238,7 +238,7 @@
     9.4  done
     9.5  
     9.6  
     9.7 -subsection\<open>Instantiating the Locale @{text M_DPow}\<close>
     9.8 +subsection\<open>Instantiating the Locale \<open>M_DPow\<close>\<close>
     9.9  
    9.10  subsubsection\<open>The Instance of Separation\<close>
    9.11  
    9.12 @@ -510,7 +510,7 @@
    9.13  
    9.14  definition
    9.15    is_Lset :: "[i=>o, i, i] => o" where
    9.16 -   --\<open>We can use the term language below because @{term is_Lset} will
    9.17 +   \<comment>\<open>We can use the term language below because @{term is_Lset} will
    9.18         not have to be internalized: it isn't used in any instance of
    9.19         separation.\<close>
    9.20     "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
    9.21 @@ -531,7 +531,7 @@
    9.22  done
    9.23  
    9.24  
    9.25 -subsection\<open>Instantiating the Locale @{text M_Lset}\<close>
    9.26 +subsection\<open>Instantiating the Locale \<open>M_Lset\<close>\<close>
    9.27  
    9.28  subsubsection\<open>The First Instance of Replacement\<close>
    9.29  
    9.30 @@ -570,7 +570,7 @@
    9.31                        is_DPow'(##Lset(i),gy,z), r) & 
    9.32                        big_union(##Lset(i),r,u), mr, v, y))]" 
    9.33  apply (simp only: rex_setclass_is_bex [symmetric])
    9.34 -  --\<open>Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body
    9.35 +  \<comment>\<open>Convert \<open>\<exists>y\<in>Lset(i)\<close> to \<open>\<exists>y[##Lset(i)]\<close> within the body
    9.36         of the @{term is_wfrec} application.\<close>
    9.37  apply (intro FOL_reflections function_reflections 
    9.38            is_wfrec_reflection Replace_reflection DPow'_reflection) 
    9.39 @@ -593,7 +593,7 @@
    9.40  done
    9.41  
    9.42  
    9.43 -subsubsection\<open>Actually Instantiating @{text M_Lset}\<close>
    9.44 +subsubsection\<open>Actually Instantiating \<open>M_Lset\<close>\<close>
    9.45  
    9.46  lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
    9.47    apply (rule M_Lset_axioms.intro)
    10.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Dec 07 10:19:30 2015 +0100
    10.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Dec 07 10:23:50 2015 +0100
    10.3 @@ -493,7 +493,7 @@
    10.4                 list_replacement2' relation1_def
    10.5                 iterates_closed [of "is_list_functor(M,A)"])
    10.6  
    10.7 -text\<open>WARNING: use only with @{text "dest:"} or with variables fixed!\<close>
    10.8 +text\<open>WARNING: use only with \<open>dest:\<close> or with variables fixed!\<close>
    10.9  lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
   10.10  
   10.11  lemma (in M_datatypes) list_N_abs [simp]:
   10.12 @@ -574,7 +574,7 @@
   10.13  done
   10.14  
   10.15  
   10.16 -subsection\<open>Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator\<close>
   10.17 +subsection\<open>Absoluteness for \<open>\<epsilon>\<close>-Closure: the @{term eclose} Operator\<close>
   10.18  
   10.19  text\<open>Re-expresses eclose using "iterates"\<close>
   10.20  lemma eclose_eq_Union:
   10.21 @@ -664,7 +664,7 @@
   10.22         wfrec_replacement(M,MH,mesa)"
   10.23  
   10.24  text\<open>The condition @{term "Ord(i)"} lets us use the simpler
   10.25 -  @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   10.26 +  \<open>trans_wfrec_abs\<close> rather than \<open>trans_wfrec_abs\<close>,
   10.27    which I haven't even proved yet.\<close>
   10.28  theorem (in M_eclose) transrec_abs:
   10.29    "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   10.30 @@ -765,7 +765,7 @@
   10.31  
   10.32  definition
   10.33    is_Member :: "[i=>o,i,i,i] => o" where
   10.34 -     --\<open>because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}\<close>
   10.35 +     \<comment>\<open>because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}\<close>
   10.36      "is_Member(M,x,y,Z) ==
   10.37          \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)"
   10.38  
   10.39 @@ -779,7 +779,7 @@
   10.40  
   10.41  definition
   10.42    is_Equal :: "[i=>o,i,i,i] => o" where
   10.43 -     --\<open>because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}\<close>
   10.44 +     \<comment>\<open>because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}\<close>
   10.45      "is_Equal(M,x,y,Z) ==
   10.46          \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)"
   10.47  
   10.48 @@ -792,7 +792,7 @@
   10.49  
   10.50  definition
   10.51    is_Nand :: "[i=>o,i,i,i] => o" where
   10.52 -     --\<open>because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}\<close>
   10.53 +     \<comment>\<open>because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}\<close>
   10.54      "is_Nand(M,x,y,Z) ==
   10.55          \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)"
   10.56  
   10.57 @@ -805,7 +805,7 @@
   10.58  
   10.59  definition
   10.60    is_Forall :: "[i=>o,i,i] => o" where
   10.61 -     --\<open>because @{term "Forall(x) \<equiv> Inr(Inr(p))"}\<close>
   10.62 +     \<comment>\<open>because @{term "Forall(x) \<equiv> Inr(Inr(p))"}\<close>
   10.63      "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
   10.64  
   10.65  lemma (in M_trivial) Forall_abs [simp]:
   10.66 @@ -821,7 +821,7 @@
   10.67  
   10.68  definition
   10.69    formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" where
   10.70 -    --\<open>the instance of @{term formula_case} in @{term formula_rec}\<close>
   10.71 +    \<comment>\<open>the instance of @{term formula_case} in @{term formula_rec}\<close>
   10.72     "formula_rec_case(a,b,c,d,h) ==
   10.73          formula_case (a, b,
   10.74                  \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
   10.75 @@ -881,7 +881,7 @@
   10.76  definition
   10.77   is_formula_case ::
   10.78      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" where
   10.79 -  --\<open>no constraint on non-formulas\<close>
   10.80 +  \<comment>\<open>no constraint on non-formulas\<close>
   10.81    "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
   10.82        (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) \<longrightarrow> finite_ordinal(M,y) \<longrightarrow>
   10.83                        is_Member(M,x,y,p) \<longrightarrow> is_a(x,y,z)) &
   10.84 @@ -915,7 +915,7 @@
   10.85  
   10.86  definition
   10.87    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" where
   10.88 -    --\<open>predicate to relativize the functional @{term formula_rec}\<close>
   10.89 +    \<comment>\<open>predicate to relativize the functional @{term formula_rec}\<close>
   10.90     "is_formula_rec(M,MH,p,z)  ==
   10.91        \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
   10.92               successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
    11.1 --- a/src/ZF/Constructible/Formula.thy	Mon Dec 07 10:19:30 2015 +0100
    11.2 +++ b/src/ZF/Constructible/Formula.thy	Mon Dec 07 10:23:50 2015 +0100
    11.3 @@ -505,13 +505,13 @@
    11.4  
    11.5  subsection\<open>Internalized Formulas for the Ordinals\<close>
    11.6  
    11.7 -text\<open>The @{text sats} theorems below differ from the usual form in that they
    11.8 +text\<open>The \<open>sats\<close> theorems below differ from the usual form in that they
    11.9  include an element of absoluteness.  That is, they relate internalized
   11.10  formulas to real concepts such as the subset relation, rather than to the
   11.11 -relativized concepts defined in theory @{text Relative}.  This lets us prove
   11.12 -the theorem as @{text Ords_in_DPow} without first having to instantiate the
   11.13 -locale @{text M_trivial}.  Note that the present theory does not even take
   11.14 -@{text Relative} as a parent.\<close>
   11.15 +relativized concepts defined in theory \<open>Relative\<close>.  This lets us prove
   11.16 +the theorem as \<open>Ords_in_DPow\<close> without first having to instantiate the
   11.17 +locale \<open>M_trivial\<close>.  Note that the present theory does not even take
   11.18 +\<open>Relative\<close> as a parent.\<close>
   11.19  
   11.20  subsubsection\<open>The subset relation\<close>
   11.21  
   11.22 @@ -578,7 +578,7 @@
   11.23  done
   11.24  
   11.25  text\<open>The subset consisting of the ordinals is definable.  Essential lemma for
   11.26 -@{text Ord_in_Lset}.  This result is the objective of the present subsection.\<close>
   11.27 +\<open>Ord_in_Lset\<close>.  This result is the objective of the present subsection.\<close>
   11.28  theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
   11.29  apply (simp add: DPow_def Collect_subset)
   11.30  apply (rule_tac x=Nil in bexI)
   11.31 @@ -594,7 +594,7 @@
   11.32    "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
   11.33  
   11.34  definition
   11.35 -  L :: "i=>o" where --\<open>Kunen's definition VI 1.5, page 167\<close>
   11.36 +  L :: "i=>o" where \<comment>\<open>Kunen's definition VI 1.5, page 167\<close>
   11.37    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
   11.38  
   11.39  text\<open>NOT SUITABLE FOR REWRITING -- RECURSIVE!\<close>
   11.40 @@ -837,7 +837,7 @@
   11.41  
   11.42  text\<open>The rank function for the constructible universe\<close>
   11.43  definition
   11.44 -  lrank :: "i=>i" where --\<open>Kunen's definition VI 1.7\<close>
   11.45 +  lrank :: "i=>i" where \<comment>\<open>Kunen's definition VI 1.7\<close>
   11.46    "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
   11.47  
   11.48  lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
    12.1 --- a/src/ZF/Constructible/Internalize.thy	Mon Dec 07 10:19:30 2015 +0100
    12.2 +++ b/src/ZF/Constructible/Internalize.thy	Mon Dec 07 10:23:50 2015 +0100
    12.3 @@ -634,7 +634,7 @@
    12.4  
    12.5  text\<open>The additional variable in the premise, namely @{term f'}, is essential.
    12.6  It lets @{term MH} depend upon @{term x}, which seems often necessary.
    12.7 -The same thing occurs in @{text is_wfrec_reflection}.\<close>
    12.8 +The same thing occurs in \<open>is_wfrec_reflection\<close>.\<close>
    12.9  theorem is_recfun_reflection:
   12.10    assumes MH_reflection:
   12.11      "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
    13.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Dec 07 10:19:30 2015 +0100
    13.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Dec 07 10:23:50 2015 +0100
    13.3 @@ -6,7 +6,7 @@
    13.4  
    13.5  theory L_axioms imports Formula Relative Reflection MetaExists begin
    13.6  
    13.7 -text \<open>The class L satisfies the premises of locale @{text M_trivial}\<close>
    13.8 +text \<open>The class L satisfies the premises of locale \<open>M_trivial\<close>\<close>
    13.9  
   13.10  lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
   13.11  apply (insert Transset_Lset)
   13.12 @@ -78,7 +78,7 @@
   13.13  apply (simp_all add: Replace_iff univalent_def, blast)
   13.14  done
   13.15  
   13.16 -subsection\<open>Instantiating the locale @{text M_trivial}\<close>
   13.17 +subsection\<open>Instantiating the locale \<open>M_trivial\<close>\<close>
   13.18  text\<open>No instances of Separation yet.\<close>
   13.19  
   13.20  lemma Lset_mono_le: "mono_le_subset(Lset)"
   13.21 @@ -110,7 +110,7 @@
   13.22  ...and dozens of similar ones.
   13.23  *)
   13.24  
   13.25 -subsection\<open>Instantiation of the locale @{text reflection}\<close>
   13.26 +subsection\<open>Instantiation of the locale \<open>reflection\<close>\<close>
   13.27  
   13.28  text\<open>instances of locale constants\<close>
   13.29  
   13.30 @@ -224,7 +224,7 @@
   13.31  done
   13.32  
   13.33  text\<open>This version handles an alternative form of the bounded quantifier
   13.34 -      in the second argument of @{text REFLECTS}.\<close>
   13.35 +      in the second argument of \<open>REFLECTS\<close>.\<close>
   13.36  theorem Rex_reflection':
   13.37       "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   13.38        ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]"
   13.39 @@ -564,11 +564,11 @@
   13.40  
   13.41  subsubsection\<open>Variants of Satisfaction Definitions for Ordinals, etc.\<close>
   13.42  
   13.43 -text\<open>The @{text sats} theorems below are standard versions of the ones proved
   13.44 -in theory @{text Formula}.  They relate elements of type @{term formula} to
   13.45 +text\<open>The \<open>sats\<close> theorems below are standard versions of the ones proved
   13.46 +in theory \<open>Formula\<close>.  They relate elements of type @{term formula} to
   13.47  relativized concepts such as @{term subset} or @{term ordinal} rather than to
   13.48  real concepts such as @{term Ord}.  Now that we have instantiated the locale
   13.49 -@{text M_trivial}, we no longer require the earlier versions.\<close>
   13.50 +\<open>M_trivial\<close>, we no longer require the earlier versions.\<close>
   13.51  
   13.52  lemma sats_subset_fm':
   13.53     "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
    14.1 --- a/src/ZF/Constructible/Normal.thy	Mon Dec 07 10:19:30 2015 +0100
    14.2 +++ b/src/ZF/Constructible/Normal.thy	Mon Dec 07 10:23:50 2015 +0100
    14.3 @@ -80,8 +80,8 @@
    14.4  text\<open>The constructions below come from Kunen, \emph{Set Theory}, page 78.\<close>
    14.5  locale cub_family =
    14.6    fixes P and A
    14.7 -  fixes next_greater -- "the next ordinal satisfying class @{term A}"
    14.8 -  fixes sup_greater  -- "sup of those ordinals over all @{term A}"
    14.9 +  fixes next_greater \<comment> "the next ordinal satisfying class @{term A}"
   14.10 +  fixes sup_greater  \<comment> "sup of those ordinals over all @{term A}"
   14.11    assumes closed:    "a\<in>A ==> Closed(P(a))"
   14.12        and unbounded: "a\<in>A ==> Unbounded(P(a))"
   14.13        and A_non0: "A\<noteq>0"
   14.14 @@ -335,7 +335,7 @@
   14.15  apply (frule lt_Ord) 
   14.16  apply (simp add: iterates_omega_def)
   14.17  apply (rule increasing_LimitI) 
   14.18 -   --"this lemma is @{thm increasing_LimitI [no_vars]}"
   14.19 +   \<comment>"this lemma is @{thm increasing_LimitI [no_vars]}"
   14.20   apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
   14.21                       Ord_UN Ord_iterates lt_imp_0_lt
   14.22                       iterates_Normal_increasing, clarify)
   14.23 @@ -382,11 +382,11 @@
   14.24                Normal_imp_fp_Unbounded)
   14.25  
   14.26  
   14.27 -subsubsection\<open>Function @{text normalize}\<close>
   14.28 +subsubsection\<open>Function \<open>normalize\<close>\<close>
   14.29  
   14.30 -text\<open>Function @{text normalize} maps a function @{text F} to a 
   14.31 +text\<open>Function \<open>normalize\<close> maps a function \<open>F\<close> to a 
   14.32        normal function that bounds it above.  The result is normal if and
   14.33 -      only if @{text F} is continuous: succ is not bounded above by any 
   14.34 +      only if \<open>F\<close> is continuous: succ is not bounded above by any 
   14.35        normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
   14.36  \<close>
   14.37  definition
    15.1 --- a/src/ZF/Constructible/Rank.thy	Mon Dec 07 10:19:30 2015 +0100
    15.2 +++ b/src/ZF/Constructible/Rank.thy	Mon Dec 07 10:23:50 2015 +0100
    15.3 @@ -15,7 +15,7 @@
    15.4        ==> separation (M, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[M]. (\<exists>p[M].
    15.5                       fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
    15.6    and obase_separation:
    15.7 -     --\<open>part of the order type formalization\<close>
    15.8 +     \<comment>\<open>part of the order type formalization\<close>
    15.9       "[| M(A); M(r) |]
   15.10        ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
   15.11               ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   15.12 @@ -92,7 +92,7 @@
   15.13  text\<open>Following Kunen's Theorem I 7.6, page 17.  Note that this material is
   15.14  not required elsewhere.\<close>
   15.15  
   15.16 -text\<open>Can't use @{text well_ord_iso_preserving} because it needs the
   15.17 +text\<open>Can't use \<open>well_ord_iso_preserving\<close> because it needs the
   15.18  strong premise @{term "well_ord(A,r)"}\<close>
   15.19  lemma (in M_ordertype) ord_iso_pred_imp_lt:
   15.20       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   15.21 @@ -114,7 +114,7 @@
   15.22  apply (frule restrict_ord_iso2, assumption+) 
   15.23  apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
   15.24  apply (frule apply_type, blast intro: ltD) 
   15.25 -  --\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
   15.26 +  \<comment>\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
   15.27  apply (simp add: pred_iff) 
   15.28  apply (subgoal_tac
   15.29         "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 
   15.30 @@ -137,26 +137,26 @@
   15.31  
   15.32  definition  
   15.33    obase :: "[i=>o,i,i] => i" where
   15.34 -       --\<open>the domain of @{text om}, eventually shown to equal @{text A}\<close>
   15.35 +       \<comment>\<open>the domain of \<open>om\<close>, eventually shown to equal \<open>A\<close>\<close>
   15.36     "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
   15.37                            g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
   15.38  
   15.39  definition
   15.40    omap :: "[i=>o,i,i,i] => o" where
   15.41 -    --\<open>the function that maps wosets to order types\<close>
   15.42 +    \<comment>\<open>the function that maps wosets to order types\<close>
   15.43     "omap(M,A,r,f) == 
   15.44          \<forall>z[M].
   15.45           z \<in> f \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
   15.46                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
   15.47  
   15.48  definition
   15.49 -  otype :: "[i=>o,i,i,i] => o" where --\<open>the order types themselves\<close>
   15.50 +  otype :: "[i=>o,i,i,i] => o" where \<comment>\<open>the order types themselves\<close>
   15.51     "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
   15.52  
   15.53  
   15.54  text\<open>Can also be proved with the premise @{term "M(z)"} instead of
   15.55        @{term "M(f)"}, but that version is less useful.  This lemma
   15.56 -      is also more useful than the definition, @{text omap_def}.\<close>
   15.57 +      is also more useful than the definition, \<open>omap_def\<close>.\<close>
   15.58  lemma (in M_ordertype) omap_iff:
   15.59       "[| omap(M,A,r,f); M(A); M(f) |] 
   15.60        ==> z \<in> f \<longleftrightarrow>
   15.61 @@ -478,7 +478,7 @@
   15.62  
   15.63  
   15.64  
   15.65 -text\<open>@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF\<close>
   15.66 +text\<open>\<open>is_oadd_fun\<close>: Relating the pure "language of set theory" to Isabelle/ZF\<close>
   15.67  lemma (in M_ord_arith) is_oadd_fun_iff:
   15.68     "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
   15.69      ==> is_oadd_fun(M,i,j,a,f) \<longleftrightarrow>
   15.70 @@ -602,7 +602,7 @@
   15.71      "[| M(i); M(x); M(g); function(g) |] 
   15.72       ==> M(THE z. omult_eqns(i, x, g, z))"
   15.73  apply (case_tac "Ord(x)")
   15.74 - prefer 2 apply (simp add: omult_eqns_Not) --\<open>trivial, non-Ord case\<close>
   15.75 + prefer 2 apply (simp add: omult_eqns_Not) \<comment>\<open>trivial, non-Ord case\<close>
   15.76  apply (erule Ord_cases) 
   15.77    apply (simp add: omult_eqns_0)
   15.78   apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
   15.79 @@ -897,12 +897,12 @@
   15.80  apply (frule is_recfun_restrict [of concl: "r^+" a])
   15.81      apply (rule trans_trancl, assumption)
   15.82     apply (simp_all add: r_into_trancl trancl_subset_times)
   15.83 -txt\<open>Still the same goal, but with new @{text is_recfun} assumptions.\<close>
   15.84 +txt\<open>Still the same goal, but with new \<open>is_recfun\<close> assumptions.\<close>
   15.85  apply (simp add: wellfoundedrank_eq)
   15.86  apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
   15.87     apply (simp_all add: transM [of a])
   15.88  txt\<open>We have used equations for wellfoundedrank and now must use some
   15.89 -    for  @{text is_recfun}.\<close>
   15.90 +    for  \<open>is_recfun\<close>.\<close>
   15.91  apply (rule_tac a=a in rangeI)
   15.92  apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
   15.93                   r_into_trancl apply_recfun r_into_trancl)
    16.1 --- a/src/ZF/Constructible/Rank_Separation.thy	Mon Dec 07 10:19:30 2015 +0100
    16.2 +++ b/src/ZF/Constructible/Rank_Separation.thy	Mon Dec 07 10:23:50 2015 +0100
    16.3 @@ -9,10 +9,10 @@
    16.4  
    16.5  
    16.6  text\<open>This theory proves all instances needed for locales
    16.7 - @{text "M_ordertype"} and  @{text "M_wfrank"}.  But the material is not
    16.8 + \<open>M_ordertype\<close> and  \<open>M_wfrank\<close>.  But the material is not
    16.9   needed for proving the relative consistency of AC.\<close>
   16.10  
   16.11 -subsection\<open>The Locale @{text "M_ordertype"}\<close>
   16.12 +subsection\<open>The Locale \<open>M_ordertype\<close>\<close>
   16.13  
   16.14  subsubsection\<open>Separation for Order-Isomorphisms\<close>
   16.15  
   16.16 @@ -46,7 +46,7 @@
   16.17  by (intro FOL_reflections function_reflections fun_plus_reflections)
   16.18  
   16.19  lemma obase_separation:
   16.20 -     --\<open>part of the order type formalization\<close>
   16.21 +     \<comment>\<open>part of the order type formalization\<close>
   16.22       "[| L(A); L(r) |]
   16.23        ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
   16.24               ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
   16.25 @@ -109,7 +109,7 @@
   16.26  
   16.27  
   16.28  
   16.29 -subsection\<open>Instantiating the locale @{text M_ordertype}\<close>
   16.30 +subsection\<open>Instantiating the locale \<open>M_ordertype\<close>\<close>
   16.31  text\<open>Separation (and Strong Replacement) for basic set-theoretic constructions
   16.32  such as intersection, Cartesian Product and image.\<close>
   16.33  
   16.34 @@ -127,7 +127,7 @@
   16.35    done
   16.36  
   16.37  
   16.38 -subsection\<open>The Locale @{text "M_wfrank"}\<close>
   16.39 +subsection\<open>The Locale \<open>M_wfrank\<close>\<close>
   16.40  
   16.41  subsubsection\<open>Separation for @{term "wfrank"}\<close>
   16.42  
   16.43 @@ -182,7 +182,7 @@
   16.44  done
   16.45  
   16.46  
   16.47 -subsubsection\<open>Separation for Proving @{text Ord_wfrank_range}\<close>
   16.48 +subsubsection\<open>Separation for Proving \<open>Ord_wfrank_range\<close>\<close>
   16.49  
   16.50  lemma Ord_wfrank_Reflects:
   16.51   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
   16.52 @@ -213,7 +213,7 @@
   16.53  done
   16.54  
   16.55  
   16.56 -subsubsection\<open>Instantiating the locale @{text M_wfrank}\<close>
   16.57 +subsubsection\<open>Instantiating the locale \<open>M_wfrank\<close>\<close>
   16.58  
   16.59  lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)"
   16.60    apply (rule M_wfrank_axioms.intro)
    17.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Dec 07 10:19:30 2015 +0100
    17.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Dec 07 10:23:50 2015 +0100
    17.3 @@ -6,14 +6,13 @@
    17.4  
    17.5  theory Rec_Separation imports Separation Internalize begin
    17.6  
    17.7 -text\<open>This theory proves all instances needed for locales @{text
    17.8 -"M_trancl"} and @{text "M_datatypes"}\<close>
    17.9 +text\<open>This theory proves all instances needed for locales \<open>M_trancl\<close> and \<open>M_datatypes\<close>\<close>
   17.10  
   17.11  lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
   17.12  by simp
   17.13  
   17.14  
   17.15 -subsection\<open>The Locale @{text "M_trancl"}\<close>
   17.16 +subsection\<open>The Locale \<open>M_trancl\<close>\<close>
   17.17  
   17.18  subsubsection\<open>Separation for Reflexive/Transitive Closure\<close>
   17.19  
   17.20 @@ -152,7 +151,7 @@
   17.21  done
   17.22  
   17.23  
   17.24 -subsubsection\<open>Separation for the Proof of @{text "wellfounded_on_trancl"}\<close>
   17.25 +subsubsection\<open>Separation for the Proof of \<open>wellfounded_on_trancl\<close>\<close>
   17.26  
   17.27  lemma wellfounded_trancl_reflects:
   17.28    "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
   17.29 @@ -175,7 +174,7 @@
   17.30  done
   17.31  
   17.32  
   17.33 -subsubsection\<open>Instantiating the locale @{text M_trancl}\<close>
   17.34 +subsubsection\<open>Instantiating the locale \<open>M_trancl\<close>\<close>
   17.35  
   17.36  lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
   17.37    apply (rule M_trancl_axioms.intro)
   17.38 @@ -356,7 +355,7 @@
   17.39  done
   17.40  
   17.41  
   17.42 -subsubsection\<open>Instantiating the locale @{text M_datatypes}\<close>
   17.43 +subsubsection\<open>Instantiating the locale \<open>M_datatypes\<close>\<close>
   17.44  
   17.45  lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
   17.46    apply (rule M_datatypes_axioms.intro)
   17.47 @@ -422,7 +421,7 @@
   17.48  done
   17.49  
   17.50  
   17.51 -subsubsection\<open>Instantiating the locale @{text M_eclose}\<close>
   17.52 +subsubsection\<open>Instantiating the locale \<open>M_eclose\<close>\<close>
   17.53  
   17.54  lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
   17.55    apply (rule M_eclose_axioms.intro)
    18.1 --- a/src/ZF/Constructible/Reflection.thy	Mon Dec 07 10:19:30 2015 +0100
    18.2 +++ b/src/ZF/Constructible/Reflection.thy	Mon Dec 07 10:23:50 2015 +0100
    18.3 @@ -19,15 +19,15 @@
    18.4  
    18.5  subsection\<open>Basic Definitions\<close>
    18.6  
    18.7 -text\<open>First part: the cumulative hierarchy defining the class @{text M}.
    18.8 -To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
    18.9 -closed under ordered pairing provided @{text l} is limit.  Possibly this
   18.10 +text\<open>First part: the cumulative hierarchy defining the class \<open>M\<close>.
   18.11 +To avoid handling multiple arguments, we assume that \<open>Mset(l)\<close> is
   18.12 +closed under ordered pairing provided \<open>l\<close> is limit.  Possibly this
   18.13  could be avoided: the induction hypothesis @{term Cl_reflects}
   18.14 -(in locale @{text ex_reflection}) could be weakened to
   18.15 +(in locale \<open>ex_reflection\<close>) could be weakened to
   18.16  @{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)"}, removing most
   18.17  uses of @{term Pair_in_Mset}.  But there isn't much point in doing so, since
   18.18 -ultimately the @{text ex_reflection} proof is packaged up using the
   18.19 -predicate @{text Reflects}.
   18.20 +ultimately the \<open>ex_reflection\<close> proof is packaged up using the
   18.21 +predicate \<open>Reflects\<close>.
   18.22  \<close>
   18.23  locale reflection =
   18.24    fixes Mset and M and Reflects
   18.25 @@ -38,9 +38,9 @@
   18.26    defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)"
   18.27        and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
   18.28                                (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)))"
   18.29 -  fixes F0 --\<open>ordinal for a specific value @{term y}\<close>
   18.30 -  fixes FF --\<open>sup over the whole level, @{term "y\<in>Mset(a)"}\<close>
   18.31 -  fixes ClEx --\<open>Reflecting ordinals for the formula @{term "\<exists>z. P"}\<close>
   18.32 +  fixes F0 \<comment>\<open>ordinal for a specific value @{term y}\<close>
   18.33 +  fixes FF \<comment>\<open>sup over the whole level, @{term "y\<in>Mset(a)"}\<close>
   18.34 +  fixes ClEx \<comment>\<open>Reflecting ordinals for the formula @{term "\<exists>z. P"}\<close>
   18.35    defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) \<longrightarrow>
   18.36                                 (\<exists>z\<in>Mset(b). P(<y,z>))"
   18.37        and "FF(P)   == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
   18.38 @@ -51,7 +51,7 @@
   18.39  apply (simp add: mono_le_subset_def leI)
   18.40  done
   18.41  
   18.42 -text\<open>Awkward: we need a version of @{text ClEx_def} as an equality
   18.43 +text\<open>Awkward: we need a version of \<open>ClEx_def\<close> as an equality
   18.44        at the level of classes, which do not really exist\<close>
   18.45  lemma (in reflection) ClEx_eq:
   18.46       "ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a"
   18.47 @@ -136,9 +136,9 @@
   18.48  text\<open>Locale for the induction hypothesis\<close>
   18.49  
   18.50  locale ex_reflection = reflection +
   18.51 -  fixes P  --"the original formula"
   18.52 -  fixes Q  --"the reflected formula"
   18.53 -  fixes Cl --"the class of reflecting ordinals"
   18.54 +  fixes P  \<comment>"the original formula"
   18.55 +  fixes Q  \<comment>"the reflected formula"
   18.56 +  fixes Cl \<comment>"the class of reflecting ordinals"
   18.57    assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)"
   18.58  
   18.59  lemma (in ex_reflection) ClEx_downward:
   18.60 @@ -159,7 +159,7 @@
   18.61               intro: Limit_is_Ord Pair_in_Mset)
   18.62  done
   18.63  
   18.64 -text\<open>Class @{text ClEx} indeed consists of reflecting ordinals...\<close>
   18.65 +text\<open>Class \<open>ClEx\<close> indeed consists of reflecting ordinals...\<close>
   18.66  lemma (in ex_reflection) ZF_ClEx_iff:
   18.67       "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |]
   18.68        ==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
   18.69 @@ -173,9 +173,9 @@
   18.70                     Closed_Unbounded_Limit Normal_normalize)
   18.71  done
   18.72  
   18.73 -text\<open>The same two theorems, exported to locale @{text reflection}.\<close>
   18.74 +text\<open>The same two theorems, exported to locale \<open>reflection\<close>.\<close>
   18.75  
   18.76 -text\<open>Class @{text ClEx} indeed consists of reflecting ordinals...\<close>
   18.77 +text\<open>Class \<open>ClEx\<close> indeed consists of reflecting ordinals...\<close>
   18.78  lemma (in reflection) ClEx_iff:
   18.79       "[| y\<in>Mset(a); Cl(a); ClEx(P,a);
   18.80          !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x) |]
   18.81 @@ -266,7 +266,7 @@
   18.82  subsection\<open>Simple Examples of Reflection\<close>
   18.83  
   18.84  text\<open>Example 1: reflecting a simple formula.  The reflecting class is first
   18.85 -given as the variable @{text ?Cl} and later retrieved from the final
   18.86 +given as the variable \<open>?Cl\<close> and later retrieved from the final
   18.87  proof state.\<close>
   18.88  schematic_goal (in reflection)
   18.89       "Reflects(?Cl,
   18.90 @@ -349,7 +349,7 @@
   18.91                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
   18.92  by fast
   18.93  
   18.94 -text\<open>Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
   18.95 +text\<open>Example 4: Axiom of Choice.  Possibly wrong, since \<open>\<Pi>\<close> needs
   18.96  to be relativized.\<close>
   18.97  schematic_goal (in reflection)
   18.98       "Reflects(?Cl,
    19.1 --- a/src/ZF/Constructible/Relative.thy	Mon Dec 07 10:19:30 2015 +0100
    19.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Dec 07 10:23:50 2015 +0100
    19.3 @@ -123,7 +123,7 @@
    19.4  
    19.5  definition
    19.6    is_range :: "[i=>o,i,i] => o" where
    19.7 -    --\<open>the cleaner
    19.8 +    \<comment>\<open>the cleaner
    19.9        @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
   19.10        unfortunately needs an instance of separation in order to prove
   19.11          @{term "M(converse(r))"}.\<close>
   19.12 @@ -200,32 +200,32 @@
   19.13  
   19.14  definition
   19.15    ordinal :: "[i=>o,i] => o" where
   19.16 -     --\<open>an ordinal is a transitive set of transitive sets\<close>
   19.17 +     \<comment>\<open>an ordinal is a transitive set of transitive sets\<close>
   19.18      "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> transitive_set(M,x))"
   19.19  
   19.20  definition
   19.21    limit_ordinal :: "[i=>o,i] => o" where
   19.22 -    --\<open>a limit ordinal is a non-empty, successor-closed ordinal\<close>
   19.23 +    \<comment>\<open>a limit ordinal is a non-empty, successor-closed ordinal\<close>
   19.24      "limit_ordinal(M,a) ==
   19.25          ordinal(M,a) & ~ empty(M,a) &
   19.26          (\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   19.27  
   19.28  definition
   19.29    successor_ordinal :: "[i=>o,i] => o" where
   19.30 -    --\<open>a successor ordinal is any ordinal that is neither empty nor limit\<close>
   19.31 +    \<comment>\<open>a successor ordinal is any ordinal that is neither empty nor limit\<close>
   19.32      "successor_ordinal(M,a) ==
   19.33          ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   19.34  
   19.35  definition
   19.36    finite_ordinal :: "[i=>o,i] => o" where
   19.37 -    --\<open>an ordinal is finite if neither it nor any of its elements are limit\<close>
   19.38 +    \<comment>\<open>an ordinal is finite if neither it nor any of its elements are limit\<close>
   19.39      "finite_ordinal(M,a) ==
   19.40          ordinal(M,a) & ~ limit_ordinal(M,a) &
   19.41          (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
   19.42  
   19.43  definition
   19.44    omega :: "[i=>o,i] => o" where
   19.45 -    --\<open>omega is a limit ordinal none of whose elements are limit\<close>
   19.46 +    \<comment>\<open>omega is a limit ordinal none of whose elements are limit\<close>
   19.47      "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
   19.48  
   19.49  definition
   19.50 @@ -245,7 +245,7 @@
   19.51  
   19.52  definition
   19.53    Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
   19.54 -    --\<open>as above, but typed\<close>
   19.55 +    \<comment>\<open>as above, but typed\<close>
   19.56      "Relation1(M,A,is_f,f) ==
   19.57          \<forall>x[M]. \<forall>y[M]. x\<in>A \<longrightarrow> is_f(x,y) \<longleftrightarrow> y = f(x)"
   19.58  
   19.59 @@ -294,9 +294,9 @@
   19.60  
   19.61  definition
   19.62    separation :: "[i=>o, i=>o] => o" where
   19.63 -    --\<open>The formula @{text P} should only involve parameters
   19.64 -        belonging to @{text M} and all its quantifiers must be relativized
   19.65 -        to @{text M}.  We do not have separation as a scheme; every instance
   19.66 +    \<comment>\<open>The formula \<open>P\<close> should only involve parameters
   19.67 +        belonging to \<open>M\<close> and all its quantifiers must be relativized
   19.68 +        to \<open>M\<close>.  We do not have separation as a scheme; every instance
   19.69          that we need must be assumed (and later proved) separately.\<close>
   19.70      "separation(M,P) ==
   19.71          \<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)"
   19.72 @@ -339,7 +339,7 @@
   19.73  subsection\<open>A trivial consistency proof for $V_\omega$\<close>
   19.74  
   19.75  text\<open>We prove that $V_\omega$
   19.76 -      (or @{text univ} in Isabelle) satisfies some ZF axioms.
   19.77 +      (or \<open>univ\<close> in Isabelle) satisfies some ZF axioms.
   19.78       Kunen, Theorem IV 3.13, page 123.\<close>
   19.79  
   19.80  lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   19.81 @@ -355,7 +355,7 @@
   19.82       "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
   19.83  by (blast intro: univ0_downwards_mem)
   19.84  
   19.85 -text\<open>Congruence rule for separation: can assume the variable is in @{text M}\<close>
   19.86 +text\<open>Congruence rule for separation: can assume the variable is in \<open>M\<close>\<close>
   19.87  lemma separation_cong [cong]:
   19.88       "(!!x. M(x) ==> P(x) \<longleftrightarrow> P'(x))
   19.89        ==> separation(M, %x. P(x)) \<longleftrightarrow> separation(M, %x. P'(x))"
   19.90 @@ -468,8 +468,8 @@
   19.91  apply (simp add: Pair_def, blast)
   19.92  done
   19.93  
   19.94 -text\<open>These two lemmas lets us prove @{text domain_closed} and
   19.95 -      @{text range_closed} without new instances of separation\<close>
   19.96 +text\<open>These two lemmas lets us prove \<open>domain_closed\<close> and
   19.97 +      \<open>range_closed\<close> without new instances of separation\<close>
   19.98  
   19.99  lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
  19.100  apply (rule equalityI, auto)
  19.101 @@ -515,7 +515,7 @@
  19.102          \<forall>y[M]. y \<in> B \<longleftrightarrow> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
  19.103  
  19.104  definition
  19.105 -  membership :: "[i=>o,i,i] => o" where --\<open>membership relation\<close>
  19.106 +  membership :: "[i=>o,i,i] => o" where \<comment>\<open>membership relation\<close>
  19.107      "membership(M,A,r) ==
  19.108          \<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
  19.109  
  19.110 @@ -534,8 +534,8 @@
  19.111        and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
  19.112  
  19.113  
  19.114 -text\<open>Automatically discovers the proof using @{text transM}, @{text nat_0I}
  19.115 -and @{text M_nat}.\<close>
  19.116 +text\<open>Automatically discovers the proof using \<open>transM\<close>, \<open>nat_0I\<close>
  19.117 +and \<open>M_nat\<close>.\<close>
  19.118  lemma (in M_trivial) nonempty [simp]: "M(0)"
  19.119  by (blast intro: transM)
  19.120  
  19.121 @@ -758,7 +758,7 @@
  19.122  lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
  19.123  by simp
  19.124  
  19.125 -text\<open>Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
  19.126 +text\<open>Better than \<open>RepFun_closed\<close> when having the formula @{term "x\<in>A"}
  19.127        makes relativization easier.\<close>
  19.128  lemma (in M_trivial) RepFun_closed2:
  19.129       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
  19.130 @@ -781,7 +781,7 @@
  19.131        ==> M(\<lambda>x\<in>A. b(x))"
  19.132  by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
  19.133  
  19.134 -text\<open>Better than @{text lam_closed}: has the formula @{term "x\<in>A"}\<close>
  19.135 +text\<open>Better than \<open>lam_closed\<close>: has the formula @{term "x\<in>A"}\<close>
  19.136  lemma (in M_trivial) lam_closed2:
  19.137    "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
  19.138       M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m))|] ==> M(Lambda(A,b))"
  19.139 @@ -816,14 +816,14 @@
  19.140   apply (blast intro!: equalityI dest: transM, blast)
  19.141  done
  19.142  
  19.143 -text\<open>What about @{text Pow_abs}?  Powerset is NOT absolute!
  19.144 +text\<open>What about \<open>Pow_abs\<close>?  Powerset is NOT absolute!
  19.145        This result is one direction of absoluteness.\<close>
  19.146  
  19.147  lemma (in M_trivial) powerset_Pow:
  19.148       "powerset(M, x, Pow(x))"
  19.149  by (simp add: powerset_def)
  19.150  
  19.151 -text\<open>But we can't prove that the powerset in @{text M} includes the
  19.152 +text\<open>But we can't prove that the powerset in \<open>M\<close> includes the
  19.153        real powerset.\<close>
  19.154  lemma (in M_trivial) powerset_imp_subset_Pow:
  19.155       "[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
  19.156 @@ -992,7 +992,7 @@
  19.157                  pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
  19.158                  upair(M,cnbf,cnbf,z))"
  19.159    and is_recfun_separation:
  19.160 -     --\<open>for well-founded recursion: used to prove @{text is_recfun_equal}\<close>
  19.161 +     \<comment>\<open>for well-founded recursion: used to prove \<open>is_recfun_equal\<close>\<close>
  19.162       "[| M(r); M(f); M(g); M(a); M(b) |]
  19.163       ==> separation(M,
  19.164              \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
  19.165 @@ -1360,7 +1360,7 @@
  19.166  
  19.167  text\<open>@{term M} contains all finite function spaces.  Needed to prove the
  19.168  absoluteness of transitive closure.  See the definition of
  19.169 -@{text rtrancl_alt} in in @{text WF_absolute.thy}.\<close>
  19.170 +\<open>rtrancl_alt\<close> in in \<open>WF_absolute.thy\<close>.\<close>
  19.171  lemma (in M_basic) finite_funspace_closed [intro,simp]:
  19.172       "[|n\<in>nat; M(B)|] ==> M(n->B)"
  19.173  apply (induct_tac n, simp)
  19.174 @@ -1428,12 +1428,12 @@
  19.175  
  19.176  definition
  19.177    is_Nil :: "[i=>o, i] => o" where
  19.178 -     --\<open>because @{prop "[] \<equiv> Inl(0)"}\<close>
  19.179 +     \<comment>\<open>because @{prop "[] \<equiv> Inl(0)"}\<close>
  19.180      "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
  19.181  
  19.182  definition
  19.183    is_Cons :: "[i=>o,i,i,i] => o" where
  19.184 -     --\<open>because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}\<close>
  19.185 +     \<comment>\<open>because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}\<close>
  19.186      "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
  19.187  
  19.188  
  19.189 @@ -1461,13 +1461,13 @@
  19.190  
  19.191  definition
  19.192    list_case' :: "[i, [i,i]=>i, i] => i" where
  19.193 -    --\<open>A version of @{term list_case} that's always defined.\<close>
  19.194 +    \<comment>\<open>A version of @{term list_case} that's always defined.\<close>
  19.195      "list_case'(a,b,xs) ==
  19.196         if quasilist(xs) then list_case(a,b,xs) else 0"
  19.197  
  19.198  definition
  19.199    is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" where
  19.200 -    --\<open>Returns 0 for non-lists\<close>
  19.201 +    \<comment>\<open>Returns 0 for non-lists\<close>
  19.202      "is_list_case(M, a, is_b, xs, z) ==
  19.203         (is_Nil(M,xs) \<longrightarrow> z=a) &
  19.204         (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) \<longrightarrow> is_b(x,l,z)) &
  19.205 @@ -1475,17 +1475,17 @@
  19.206  
  19.207  definition
  19.208    hd' :: "i => i" where
  19.209 -    --\<open>A version of @{term hd} that's always defined.\<close>
  19.210 +    \<comment>\<open>A version of @{term hd} that's always defined.\<close>
  19.211      "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
  19.212  
  19.213  definition
  19.214    tl' :: "i => i" where
  19.215 -    --\<open>A version of @{term tl} that's always defined.\<close>
  19.216 +    \<comment>\<open>A version of @{term tl} that's always defined.\<close>
  19.217      "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
  19.218  
  19.219  definition
  19.220    is_hd :: "[i=>o,i,i] => o" where
  19.221 -     --\<open>@{term "hd([]) = 0"} no constraints if not a list.
  19.222 +     \<comment>\<open>@{term "hd([]) = 0"} no constraints if not a list.
  19.223            Avoiding implication prevents the simplifier's looping.\<close>
  19.224      "is_hd(M,xs,H) ==
  19.225         (is_Nil(M,xs) \<longrightarrow> empty(M,H)) &
  19.226 @@ -1494,7 +1494,7 @@
  19.227  
  19.228  definition
  19.229    is_tl :: "[i=>o,i,i] => o" where
  19.230 -     --\<open>@{term "tl([]) = []"}; see comments about @{term is_hd}\<close>
  19.231 +     \<comment>\<open>@{term "tl([]) = []"}; see comments about @{term is_hd}\<close>
  19.232      "is_tl(M,xs,T) ==
  19.233         (is_Nil(M,xs) \<longrightarrow> T=xs) &
  19.234         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
    20.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Mon Dec 07 10:19:30 2015 +0100
    20.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Mon Dec 07 10:23:50 2015 +0100
    20.3 @@ -147,7 +147,7 @@
    20.4  
    20.5  text\<open>The second argument of @{term is_a} gives it direct access to @{term x},
    20.6    which is essential for handling free variable references.  Treatment is
    20.7 -  based on that of @{text is_nat_case_reflection}.\<close>
    20.8 +  based on that of \<open>is_nat_case_reflection\<close>.\<close>
    20.9  theorem is_formula_case_reflection:
   20.10    assumes is_a_reflection:
   20.11      "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
   20.12 @@ -176,7 +176,7 @@
   20.13  
   20.14  definition
   20.15    is_depth_apply :: "[i=>o,i,i,i] => o" where
   20.16 -   --\<open>Merely a useful abbreviation for the sequel.\<close>
   20.17 +   \<comment>\<open>Merely a useful abbreviation for the sequel.\<close>
   20.18    "is_depth_apply(M,h,p,z) ==
   20.19      \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
   20.20          finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
   20.21 @@ -190,10 +190,10 @@
   20.22  
   20.23  
   20.24  text\<open>There is at present some redundancy between the relativizations in
   20.25 - e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.\<close>
   20.26 + e.g. \<open>satisfies_is_a\<close> and those in e.g. \<open>Member_replacement\<close>.\<close>
   20.27  
   20.28  text\<open>These constants let us instantiate the parameters @{term a}, @{term b},
   20.29 -      @{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.\<close>
   20.30 +      @{term c}, @{term d}, etc., of the locale \<open>Formula_Rec\<close>.\<close>
   20.31  definition
   20.32    satisfies_a :: "[i,i,i]=>i" where
   20.33     "satisfies_a(A) == 
   20.34 @@ -216,7 +216,7 @@
   20.35  
   20.36  definition
   20.37    satisfies_is_b :: "[i=>o,i,i,i,i]=>o" where
   20.38 -   --\<open>We simplify the formula to have just @{term nx} rather than 
   20.39 +   \<comment>\<open>We simplify the formula to have just @{term nx} rather than 
   20.40         introducing @{term ny} with  @{term "nx=ny"}\<close>
   20.41    "satisfies_is_b(M,A) == 
   20.42      \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
   20.43 @@ -259,7 +259,7 @@
   20.44  
   20.45  definition
   20.46    satisfies_MH :: "[i=>o,i,i,i,i]=>o" where
   20.47 -    --\<open>The variable @{term u} is unused, but gives @{term satisfies_MH} 
   20.48 +    \<comment>\<open>The variable @{term u} is unused, but gives @{term satisfies_MH} 
   20.49          the correct arity.\<close>
   20.50    "satisfies_MH == 
   20.51      \<lambda>M A u f z. 
   20.52 @@ -327,11 +327,11 @@
   20.53                pair(M,env,bo,z))"
   20.54   and
   20.55    formula_rec_replacement: 
   20.56 -      --\<open>For the @{term transrec}\<close>
   20.57 +      \<comment>\<open>For the @{term transrec}\<close>
   20.58     "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
   20.59   and
   20.60    formula_rec_lambda_replacement:  
   20.61 -      --\<open>For the @{text "\<lambda>-abstraction"} in the @{term transrec} body\<close>
   20.62 +      \<comment>\<open>For the \<open>\<lambda>-abstraction\<close> in the @{term transrec} body\<close>
   20.63     "[|M(g); M(A)|] ==>
   20.64      strong_replacement (M, 
   20.65         \<lambda>x y. mem_formula(M,x) &
   20.66 @@ -460,7 +460,7 @@
   20.67  
   20.68  
   20.69  
   20.70 -text\<open>Instantiate locale @{text Formula_Rec} for the 
   20.71 +text\<open>Instantiate locale \<open>Formula_Rec\<close> for the 
   20.72        Function @{term satisfies}\<close>
   20.73  
   20.74  lemma (in M_satisfies) Formula_Rec_axioms_M:
   20.75 @@ -505,7 +505,7 @@
   20.76                 satisfies_eq is_satisfies_def satisfies_MH_def)
   20.77  
   20.78  
   20.79 -subsection\<open>Internalizations Needed to Instantiate @{text "M_satisfies"}\<close>
   20.80 +subsection\<open>Internalizations Needed to Instantiate \<open>M_satisfies\<close>\<close>
   20.81  
   20.82  subsubsection\<open>The Operator @{term is_depth_apply}, Internalized\<close>
   20.83  
   20.84 @@ -815,7 +815,7 @@
   20.85  done
   20.86  
   20.87  
   20.88 -subsection\<open>Lemmas for Instantiating the Locale @{text "M_satisfies"}\<close>
   20.89 +subsection\<open>Lemmas for Instantiating the Locale \<open>M_satisfies\<close>\<close>
   20.90  
   20.91  
   20.92  subsubsection\<open>The @{term "Member"} Case\<close>
   20.93 @@ -959,7 +959,7 @@
   20.94            is_wfrec_reflection) 
   20.95  
   20.96  lemma formula_rec_replacement: 
   20.97 -      --\<open>For the @{term transrec}\<close>
   20.98 +      \<comment>\<open>For the @{term transrec}\<close>
   20.99     "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
  20.100  apply (rule transrec_replacementI, simp add: nat_into_M) 
  20.101  apply (rule strong_replacementI)
  20.102 @@ -995,7 +995,7 @@
  20.103            satisfies_is_d_reflection)  
  20.104  
  20.105  lemma formula_rec_lambda_replacement: 
  20.106 -      --\<open>For the @{term transrec}\<close>
  20.107 +      \<comment>\<open>For the @{term transrec}\<close>
  20.108     "[|L(g); L(A)|] ==>
  20.109      strong_replacement (L, 
  20.110         \<lambda>x y. mem_formula(L,x) &
  20.111 @@ -1016,7 +1016,7 @@
  20.112  done
  20.113  
  20.114  
  20.115 -subsection\<open>Instantiating @{text M_satisfies}\<close>
  20.116 +subsection\<open>Instantiating \<open>M_satisfies\<close>\<close>
  20.117  
  20.118  lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
  20.119    apply (rule M_satisfies_axioms.intro)
    21.1 --- a/src/ZF/Constructible/Separation.thy	Mon Dec 07 10:19:30 2015 +0100
    21.2 +++ b/src/ZF/Constructible/Separation.thy	Mon Dec 07 10:23:50 2015 +0100
    21.3 @@ -6,7 +6,7 @@
    21.4  
    21.5  theory Separation imports L_axioms WF_absolute begin
    21.6  
    21.7 -text\<open>This theory proves all instances needed for locale @{text "M_basic"}\<close>
    21.8 +text\<open>This theory proves all instances needed for locale \<open>M_basic\<close>\<close>
    21.9  
   21.10  text\<open>Helps us solve for de Bruijn indices!\<close>
   21.11  lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
   21.12 @@ -274,7 +274,7 @@
   21.13  by (intro FOL_reflections function_reflections fun_plus_reflections)
   21.14  
   21.15  lemma is_recfun_separation:
   21.16 -     --\<open>for well-founded recursion\<close>
   21.17 +     \<comment>\<open>for well-founded recursion\<close>
   21.18       "[| L(r); L(f); L(g); L(a); L(b) |]
   21.19       ==> separation(L,
   21.20              \<lambda>x. \<exists>xa[L]. \<exists>xb[L].
   21.21 @@ -288,7 +288,7 @@
   21.22  done
   21.23  
   21.24  
   21.25 -subsection\<open>Instantiating the locale @{text M_basic}\<close>
   21.26 +subsection\<open>Instantiating the locale \<open>M_basic\<close>\<close>
   21.27  text\<open>Separation (and Strong Replacement) for basic set-theoretic constructions
   21.28  such as intersection, Cartesian Product and image.\<close>
   21.29  
    22.1 --- a/src/ZF/Constructible/WF_absolute.thy	Mon Dec 07 10:19:30 2015 +0100
    22.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Mon Dec 07 10:23:50 2015 +0100
    22.3 @@ -60,7 +60,7 @@
    22.4  
    22.5  definition
    22.6    rtran_closure_mem :: "[i=>o,i,i,i] => o" where
    22.7 -    --\<open>The property of belonging to @{text "rtran_closure(r)"}\<close>
    22.8 +    \<comment>\<open>The property of belonging to \<open>rtran_closure(r)\<close>\<close>
    22.9      "rtran_closure_mem(M,A,r,p) ==
   22.10                \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
   22.11                 omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
   22.12 @@ -140,7 +140,7 @@
   22.13       "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & <w,x> \<in> r^+)"
   22.14  by (insert wellfounded_trancl_separation [of r Z], simp) 
   22.15  
   22.16 -text\<open>Alternative proof of @{text wf_on_trancl}; inspiration for the
   22.17 +text\<open>Alternative proof of \<open>wf_on_trancl\<close>; inspiration for the
   22.18        relativized version.  Original version is on theory WF.\<close>
   22.19  lemma "[| wf[A](r);  r-``A \<subseteq> A |] ==> wf[A](r^+)"
   22.20  apply (simp add: wf_on_def wf_def)
   22.21 @@ -200,7 +200,7 @@
   22.22  done
   22.23  
   22.24  
   22.25 -text\<open>Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
   22.26 +text\<open>Assuming @{term r} is transitive simplifies the occurrences of \<open>H\<close>.
   22.27        The premise @{term "relation(r)"} is necessary 
   22.28        before we can replace @{term "r^+"} by @{term r}.\<close>
   22.29  theorem (in M_trancl) trans_wfrec_relativize:
   22.30 @@ -238,7 +238,7 @@
   22.31  
   22.32  subsection\<open>M is closed under well-founded recursion\<close>
   22.33  
   22.34 -text\<open>Lemma with the awkward premise mentioning @{text wfrec}.\<close>
   22.35 +text\<open>Lemma with the awkward premise mentioning \<open>wfrec\<close>.\<close>
   22.36  lemma (in M_trancl) wfrec_closed_lemma [rule_format]:
   22.37       "[|wf(r); M(r); 
   22.38          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
    23.1 --- a/src/ZF/Constructible/WFrec.thy	Mon Dec 07 10:19:30 2015 +0100
    23.2 +++ b/src/ZF/Constructible/WFrec.thy	Mon Dec 07 10:23:50 2015 +0100
    23.3 @@ -18,7 +18,7 @@
    23.4  apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
    23.5  done
    23.6  
    23.7 -text\<open>Expresses @{text is_recfun} as a recursion equation\<close>
    23.8 +text\<open>Expresses \<open>is_recfun\<close> as a recursion equation\<close>
    23.9  lemma is_recfun_iff_equation:
   23.10       "is_recfun(r,a,H,f) \<longleftrightarrow>
   23.11             f \<in> r -`` {a} \<rightarrow> range(f) &
   23.12 @@ -56,7 +56,7 @@
   23.13  apply (simp_all add: vimage_singleton_iff Int_lower2)  
   23.14  done
   23.15  
   23.16 -text\<open>For @{text is_recfun} we need only pay attention to functions
   23.17 +text\<open>For \<open>is_recfun\<close> we need only pay attention to functions
   23.18        whose domains are initial segments of @{term r}.\<close>
   23.19  lemma is_recfun_cong:
   23.20    "[| r = r'; a = a'; f = f'; 
   23.21 @@ -82,7 +82,7 @@
   23.22  
   23.23  text\<open>Stated using @{term "trans(r)"} rather than
   23.24        @{term "transitive_rel(M,A,r)"} because the latter rewrites to
   23.25 -      the former anyway, by @{text transitive_rel_abs}.
   23.26 +      the former anyway, by \<open>transitive_rel_abs\<close>.
   23.27        As always, theorems should be expressed in simplified form.
   23.28        The last three M-premises are redundant because of @{term "M(r)"}, 
   23.29        but without them we'd have to undertake
   23.30 @@ -130,7 +130,7 @@
   23.31  apply (blast intro!: is_recfun_equal dest: transM) 
   23.32  done 
   23.33  
   23.34 -text\<open>Tells us that @{text is_recfun} can (in principle) be relativized.\<close>
   23.35 +text\<open>Tells us that \<open>is_recfun\<close> can (in principle) be relativized.\<close>
   23.36  lemma (in M_basic) is_recfun_relativize:
   23.37    "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |] 
   23.38     ==> is_recfun(r,a,H,f) \<longleftrightarrow>
   23.39 @@ -180,7 +180,7 @@
   23.40         ==> restrict(Y, r -`` {x}) = f"
   23.41  apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y \<longleftrightarrow> <y,z>:f") 
   23.42   apply (simp (no_asm_simp) add: restrict_def) 
   23.43 - apply (thin_tac "rall(M,P)" for P)+  --\<open>essential for efficiency\<close>
   23.44 + apply (thin_tac "rall(M,P)" for P)+  \<comment>\<open>essential for efficiency\<close>
   23.45   apply (frule is_recfun_type [THEN fun_is_rel], blast)
   23.46  apply (frule pair_components_in_M, assumption, clarify) 
   23.47  apply (rule iffI)
   23.48 @@ -207,7 +207,7 @@
   23.49  done
   23.50  
   23.51  
   23.52 -text\<open>Proof of the inductive step for @{text exists_is_recfun}, since
   23.53 +text\<open>Proof of the inductive step for \<open>exists_is_recfun\<close>, since
   23.54        we must prove two versions.\<close>
   23.55  lemma (in M_basic) exists_is_recfun_indstep:
   23.56      "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r \<longrightarrow> (\<exists>f[M]. is_recfun(r, y, H, f)); 
   23.57 @@ -220,7 +220,7 @@
   23.58    apply blast 
   23.59   txt\<open>Discharge the "univalent" obligation of Replacement\<close>
   23.60   apply (simp add: univalent_is_recfun) 
   23.61 -txt\<open>Show that the constructed object satisfies @{text is_recfun}\<close> 
   23.62 +txt\<open>Show that the constructed object satisfies \<open>is_recfun\<close>\<close> 
   23.63  apply clarify 
   23.64  apply (rule_tac x=Y in rexI)  
   23.65  txt\<open>Unfold only the top-level occurrence of @{term is_recfun}\<close>
    24.1 --- a/src/ZF/Constructible/Wellorderings.thy	Mon Dec 07 10:19:30 2015 +0100
    24.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Mon Dec 07 10:23:50 2015 +0100
    24.3 @@ -9,7 +9,7 @@
    24.4  text\<open>We define functions analogous to @{term ordermap} @{term ordertype} 
    24.5        but without using recursion.  Instead, there is a direct appeal
    24.6        to Replacement.  This will be the basis for a version relativized
    24.7 -      to some class @{text M}.  The main result is Theorem I 7.6 in Kunen,
    24.8 +      to some class \<open>M\<close>.  The main result is Theorem I 7.6 in Kunen,
    24.9        page 17.\<close>
   24.10  
   24.11  
   24.12 @@ -32,18 +32,18 @@
   24.13  
   24.14  definition
   24.15    wellfounded :: "[i=>o,i]=>o" where
   24.16 -    --\<open>EVERY non-empty set has an @{text r}-minimal element\<close>
   24.17 +    \<comment>\<open>EVERY non-empty set has an \<open>r\<close>-minimal element\<close>
   24.18      "wellfounded(M,r) == 
   24.19          \<forall>x[M]. x\<noteq>0 \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
   24.20  definition
   24.21    wellfounded_on :: "[i=>o,i,i]=>o" where
   24.22 -    --\<open>every non-empty SUBSET OF @{text A} has an @{text r}-minimal element\<close>
   24.23 +    \<comment>\<open>every non-empty SUBSET OF \<open>A\<close> has an \<open>r\<close>-minimal element\<close>
   24.24      "wellfounded_on(M,A,r) == 
   24.25          \<forall>x[M]. x\<noteq>0 \<longrightarrow> x\<subseteq>A \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
   24.26  
   24.27  definition
   24.28    wellordered :: "[i=>o,i,i]=>o" where
   24.29 -    --\<open>linear and wellfounded on @{text A}\<close>
   24.30 +    \<comment>\<open>linear and wellfounded on \<open>A\<close>\<close>
   24.31      "wellordered(M,A,r) == 
   24.32          transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
   24.33  
    25.1 --- a/src/ZF/EquivClass.thy	Mon Dec 07 10:19:30 2015 +0100
    25.2 +++ b/src/ZF/EquivClass.thy	Mon Dec 07 10:23:50 2015 +0100
    25.3 @@ -27,7 +27,7 @@
    25.4  abbreviation
    25.5    RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr "respects2 " 80) where
    25.6    "f respects2 r == congruent2(r,r,f)"
    25.7 -    --\<open>Abbreviation for the common case where the relations are identical\<close>
    25.8 +    \<comment>\<open>Abbreviation for the common case where the relations are identical\<close>
    25.9  
   25.10  
   25.11  subsection\<open>Suppes, Theorem 70:
    26.1 --- a/src/ZF/IMP/Equiv.thy	Mon Dec 07 10:19:30 2015 +0100
    26.2 +++ b/src/ZF/IMP/Equiv.thy	Mon Dec 07 10:23:50 2015 +0100
    26.3 @@ -38,14 +38,14 @@
    26.4  lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
    26.5    apply (erule evalc.induct)
    26.6          apply (simp_all (no_asm_simp))
    26.7 -     txt \<open>@{text assign}\<close>
    26.8 +     txt \<open>\<open>assign\<close>\<close>
    26.9       apply (simp add: update_type)
   26.10 -    txt \<open>@{text comp}\<close>
   26.11 +    txt \<open>\<open>comp\<close>\<close>
   26.12      apply fast
   26.13 -   txt \<open>@{text while}\<close>
   26.14 +   txt \<open>\<open>while\<close>\<close>
   26.15     apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
   26.16     apply (simp add: Gamma_def)
   26.17 -  txt \<open>recursive case of @{text while}\<close>
   26.18 +  txt \<open>recursive case of \<open>while\<close>\<close>
   26.19    apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
   26.20    apply (auto simp add: Gamma_def)
   26.21    done
   26.22 @@ -56,19 +56,19 @@
   26.23  
   26.24  lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
   26.25    apply (erule com.induct)
   26.26 -      txt \<open>@{text skip}\<close>
   26.27 +      txt \<open>\<open>skip\<close>\<close>
   26.28        apply force
   26.29 -     txt \<open>@{text assign}\<close>
   26.30 +     txt \<open>\<open>assign\<close>\<close>
   26.31       apply force
   26.32 -    txt \<open>@{text comp}\<close>
   26.33 +    txt \<open>\<open>comp\<close>\<close>
   26.34      apply force
   26.35 -   txt \<open>@{text while}\<close>
   26.36 +   txt \<open>\<open>while\<close>\<close>
   26.37     apply safe
   26.38     apply simp_all
   26.39     apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
   26.40     apply (unfold Gamma_def)
   26.41     apply force
   26.42 -  txt \<open>@{text "if"}\<close>
   26.43 +  txt \<open>\<open>if\<close>\<close>
   26.44    apply auto
   26.45    done
   26.46  
    27.1 --- a/src/ZF/Induct/Acc.thy	Mon Dec 07 10:19:30 2015 +0100
    27.2 +++ b/src/ZF/Induct/Acc.thy	Mon Dec 07 10:23:50 2015 +0100
    27.3 @@ -8,7 +8,7 @@
    27.4  theory Acc imports Main begin
    27.5  
    27.6  text \<open>
    27.7 -  Inductive definition of @{text "acc(r)"}; see @{cite "paulin-tlca"}.
    27.8 +  Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
    27.9  \<close>
   27.10  
   27.11  consts
   27.12 @@ -22,7 +22,7 @@
   27.13  
   27.14  text \<open>
   27.15    The introduction rule must require @{prop "a \<in> field(r)"},
   27.16 -  otherwise @{text "acc(r)"} would be a proper class!
   27.17 +  otherwise \<open>acc(r)\<close> would be a proper class!
   27.18  
   27.19    \medskip
   27.20    The intended introduction rule:
    28.1 --- a/src/ZF/Induct/Binary_Trees.thy	Mon Dec 07 10:19:30 2015 +0100
    28.2 +++ b/src/ZF/Induct/Binary_Trees.thy	Mon Dec 07 10:23:50 2015 +0100
    28.3 @@ -21,11 +21,11 @@
    28.4    by (induct arbitrary: x r set: bt) auto
    28.5  
    28.6  lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
    28.7 -  -- "Proving a freeness theorem."
    28.8 +  \<comment> "Proving a freeness theorem."
    28.9    by (fast elim!: bt.free_elims)
   28.10  
   28.11  inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
   28.12 -  -- "An elimination rule, for type-checking."
   28.13 +  \<comment> "An elimination rule, for type-checking."
   28.14  
   28.15  text \<open>
   28.16    \medskip Lemmas to justify using @{term bt} in other recursive type
   28.17 @@ -58,7 +58,7 @@
   28.18      !!x y z r s. [| x \<in> A;  y \<in> bt(A);  z \<in> bt(A);  r \<in> C(y);  s \<in> C(z) |] ==>
   28.19      h(x, y, z, r, s) \<in> C(Br(x, y, z))
   28.20    |] ==> bt_rec(c, h, t) \<in> C(t)"
   28.21 -  -- \<open>Type checking for recursor -- example only; not really needed.\<close>
   28.22 +  \<comment> \<open>Type checking for recursor -- example only; not really needed.\<close>
   28.23    apply (induct_tac t)
   28.24     apply simp_all
   28.25    done
    29.1 --- a/src/ZF/Induct/Brouwer.thy	Mon Dec 07 10:19:30 2015 +0100
    29.2 +++ b/src/ZF/Induct/Brouwer.thy	Mon Dec 07 10:23:50 2015 +0100
    29.3 @@ -28,7 +28,7 @@
    29.4        "!!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b))"
    29.5        "!!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
    29.6    shows "P(b)"
    29.7 -  -- \<open>A nicer induction rule than the standard one.\<close>
    29.8 +  \<comment> \<open>A nicer induction rule than the standard one.\<close>
    29.9    using b
   29.10    apply induct
   29.11      apply (rule cases(1))
   29.12 @@ -45,7 +45,7 @@
   29.13    Well :: "[i, i => i] => i"
   29.14  
   29.15  datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
   29.16 -    -- \<open>The union with @{text nat} ensures that the cardinal is infinite.\<close>
   29.17 +    \<comment> \<open>The union with \<open>nat\<close> ensures that the cardinal is infinite.\<close>
   29.18    "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
   29.19    monos Pi_mono
   29.20    type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
   29.21 @@ -59,7 +59,7 @@
   29.22    assumes w: "w \<in> Well(A, B)"
   29.23      and step: "!!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
   29.24    shows "P(w)"
   29.25 -  -- \<open>A nicer induction rule than the standard one.\<close>
   29.26 +  \<comment> \<open>A nicer induction rule than the standard one.\<close>
   29.27    using w
   29.28    apply induct
   29.29    apply (assumption | rule step)+
   29.30 @@ -68,8 +68,8 @@
   29.31    done
   29.32  
   29.33  lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
   29.34 -  -- \<open>In fact it's isomorphic to @{text nat}, but we need a recursion operator\<close>
   29.35 -  -- \<open>for @{text Well} to prove this.\<close>
   29.36 +  \<comment> \<open>In fact it's isomorphic to \<open>nat\<close>, but we need a recursion operator\<close>
   29.37 +  \<comment> \<open>for \<open>Well\<close> to prove this.\<close>
   29.38    apply (rule Well_unfold [THEN trans])
   29.39    apply (simp add: Sigma_bool succ_def)
   29.40    done
    30.1 --- a/src/ZF/Induct/Comb.thy	Mon Dec 07 10:19:30 2015 +0100
    30.2 +++ b/src/ZF/Induct/Comb.thy	Mon Dec 07 10:23:50 2015 +0100
    30.3 @@ -15,7 +15,7 @@
    30.4  
    30.5  subsection \<open>Definitions\<close>
    30.6  
    30.7 -text \<open>Datatype definition of combinators @{text S} and @{text K}.\<close>
    30.8 +text \<open>Datatype definition of combinators \<open>S\<close> and \<open>K\<close>.\<close>
    30.9  
   30.10  consts comb :: i
   30.11  datatype comb =
   30.12 @@ -24,8 +24,8 @@
   30.13    | app ("p \<in> comb", "q \<in> comb")    (infixl "\<bullet>" 90)
   30.14  
   30.15  text \<open>
   30.16 -  Inductive definition of contractions, @{text "-1->"} and
   30.17 -  (multi-step) reductions, @{text "-\<longrightarrow>"}.
   30.18 +  Inductive definition of contractions, \<open>-1->\<close> and
   30.19 +  (multi-step) reductions, \<open>-\<longrightarrow>\<close>.
   30.20  \<close>
   30.21  
   30.22  consts
   30.23 @@ -49,8 +49,8 @@
   30.24    type_intros comb.intros
   30.25  
   30.26  text \<open>
   30.27 -  Inductive definition of parallel contractions, @{text "=1=>"} and
   30.28 -  (multi-step) parallel reductions, @{text "===>"}.
   30.29 +  Inductive definition of parallel contractions, \<open>=1=>\<close> and
   30.30 +  (multi-step) parallel reductions, \<open>===>\<close>.
   30.31  \<close>
   30.32  
   30.33  consts
   30.34 @@ -115,8 +115,8 @@
   30.35  subsection \<open>Results about Contraction\<close>
   30.36  
   30.37  text \<open>
   30.38 -  For type checking: replaces @{term "a -1-> b"} by @{text "a, b \<in>
   30.39 -  comb"}.
   30.40 +  For type checking: replaces @{term "a -1-> b"} by \<open>a, b \<in>
   30.41 +  comb\<close>.
   30.42  \<close>
   30.43  
   30.44  lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
   30.45 @@ -141,7 +141,7 @@
   30.46    contract.Ap2 [THEN rtrancl_into_rtrancl2]
   30.47  
   30.48  lemma "p \<in> comb ==> I\<bullet>p -\<longrightarrow> p"
   30.49 -  -- \<open>Example only: not used\<close>
   30.50 +  \<comment> \<open>Example only: not used\<close>
   30.51    by (unfold I_def) (blast intro: reduction_rls)
   30.52  
   30.53  lemma comb_I: "I \<in> comb"
   30.54 @@ -181,7 +181,7 @@
   30.55                        contract_combD2 reduction_rls)
   30.56    done
   30.57  
   30.58 -text \<open>Counterexample to the diamond property for @{text "-1->"}.\<close>
   30.59 +text \<open>Counterexample to the diamond property for \<open>-1->\<close>.\<close>
   30.60  
   30.61  lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
   30.62    by (blast intro: comb_I)
   30.63 @@ -201,8 +201,8 @@
   30.64  
   30.65  subsection \<open>Results about Parallel Contraction\<close>
   30.66  
   30.67 -text \<open>For type checking: replaces @{text "a =1=> b"} by @{text "a, b
   30.68 -  \<in> comb"}\<close>
   30.69 +text \<open>For type checking: replaces \<open>a =1=> b\<close> by \<open>a, b
   30.70 +  \<in> comb\<close>\<close>
   30.71  lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
   30.72    and parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
   30.73    and parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
   30.74 @@ -234,7 +234,7 @@
   30.75    by auto
   30.76  
   30.77  lemma diamond_parcontract: "diamond(parcontract)"
   30.78 -  -- \<open>Church-Rosser property for parallel contraction\<close>
   30.79 +  \<comment> \<open>Church-Rosser property for parallel contraction\<close>
   30.80    apply (unfold diamond_def)
   30.81    apply (rule impI [THEN allI, THEN allI])
   30.82    apply (erule parcontract.induct)
    31.1 --- a/src/ZF/Induct/Datatypes.thy	Mon Dec 07 10:19:30 2015 +0100
    31.2 +++ b/src/ZF/Induct/Datatypes.thy	Mon Dec 07 10:23:50 2015 +0100
    31.3 @@ -10,8 +10,7 @@
    31.4  subsection \<open>A type with four constructors\<close>
    31.5  
    31.6  text \<open>
    31.7 -  It has four contructors, of arities 0--3, and two parameters @{text
    31.8 -  A} and @{text B}.
    31.9 +  It has four contructors, of arities 0--3, and two parameters \<open>A\<close> and \<open>B\<close>.
   31.10  \<close>
   31.11  
   31.12  consts
    32.1 --- a/src/ZF/Induct/ListN.thy	Mon Dec 07 10:19:30 2015 +0100
    32.2 +++ b/src/ZF/Induct/ListN.thy	Mon Dec 07 10:23:50 2015 +0100
    32.3 @@ -8,7 +8,7 @@
    32.4  theory ListN imports Main begin
    32.5  
    32.6  text \<open>
    32.7 -  Inductive definition of lists of @{text n} elements; see
    32.8 +  Inductive definition of lists of \<open>n\<close> elements; see
    32.9    @{cite "paulin-tlca"}.
   32.10  \<close>
   32.11  
    33.1 --- a/src/ZF/Induct/Multiset.thy	Mon Dec 07 10:19:30 2015 +0100
    33.2 +++ b/src/ZF/Induct/Multiset.thy	Mon Dec 07 10:23:50 2015 +0100
    33.3 @@ -12,7 +12,7 @@
    33.4  begin
    33.5  
    33.6  abbreviation (input)
    33.7 -  -- \<open>Short cut for multiset space\<close>
    33.8 +  \<comment> \<open>Short cut for multiset space\<close>
    33.9    Mult :: "i=>i" where
   33.10    "Mult(A) == A -||> nat-{0}"
   33.11  
    34.1 --- a/src/ZF/Induct/Ntree.thy	Mon Dec 07 10:19:30 2015 +0100
    34.2 +++ b/src/ZF/Induct/Ntree.thy	Mon Dec 07 10:23:50 2015 +0100
    34.3 @@ -9,7 +9,7 @@
    34.4  
    34.5  text \<open>
    34.6    Demonstrates a simple use of function space in a datatype
    34.7 -  definition.  Based upon theory @{text Term}.
    34.8 +  definition.  Based upon theory \<open>Term\<close>.
    34.9  \<close>
   34.10  
   34.11  consts
   34.12 @@ -18,12 +18,12 @@
   34.13    maptree2 :: "[i, i] => i"
   34.14  
   34.15  datatype "ntree(A)" = Branch ("a \<in> A", "h \<in> (\<Union>n \<in> nat. n -> ntree(A))")
   34.16 -  monos UN_mono [OF subset_refl Pi_mono]  -- \<open>MUST have this form\<close>
   34.17 +  monos UN_mono [OF subset_refl Pi_mono]  \<comment> \<open>MUST have this form\<close>
   34.18    type_intros nat_fun_univ [THEN subsetD]
   34.19    type_elims UN_E
   34.20  
   34.21  datatype "maptree(A)" = Sons ("a \<in> A", "h \<in> maptree(A) -||> maptree(A)")
   34.22 -  monos FiniteFun_mono1  -- \<open>Use monotonicity in BOTH args\<close>
   34.23 +  monos FiniteFun_mono1  \<comment> \<open>Use monotonicity in BOTH args\<close>
   34.24    type_intros FiniteFun_univ1 [THEN subsetD]
   34.25  
   34.26  datatype "maptree2(A, B)" = Sons2 ("a \<in> A", "h \<in> B -||> maptree2(A, B)")
   34.27 @@ -41,7 +41,7 @@
   34.28  
   34.29  
   34.30  text \<open>
   34.31 -  \medskip @{text ntree}
   34.32 +  \medskip \<open>ntree\<close>
   34.33  \<close>
   34.34  
   34.35  lemma ntree_unfold: "ntree(A) = A \<times> (\<Union>n \<in> nat. n -> ntree(A))"
   34.36 @@ -53,7 +53,7 @@
   34.37      and step: "!!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  \<forall>i \<in> n. P(h`i)
   34.38        |] ==> P(Branch(x,h))"
   34.39    shows "P(t)"
   34.40 -  -- \<open>A nicer induction rule than the standard one.\<close>
   34.41 +  \<comment> \<open>A nicer induction rule than the standard one.\<close>
   34.42    using t
   34.43    apply induct
   34.44    apply (erule UN_E)
   34.45 @@ -69,7 +69,7 @@
   34.46      and step: "!!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  f O h = g O h |] ==>
   34.47        f ` Branch(x,h) = g ` Branch(x,h)"
   34.48    shows "f`t=g`t"
   34.49 -  -- \<open>Induction on @{term "ntree(A)"} to prove an equation\<close>
   34.50 +  \<comment> \<open>Induction on @{term "ntree(A)"} to prove an equation\<close>
   34.51    using t
   34.52    apply induct
   34.53    apply (assumption | rule step)+
   34.54 @@ -80,7 +80,7 @@
   34.55    done
   34.56  
   34.57  text \<open>
   34.58 -  \medskip Lemmas to justify using @{text Ntree} in other recursive
   34.59 +  \medskip Lemmas to justify using \<open>Ntree\<close> in other recursive
   34.60    type definitions.
   34.61  \<close>
   34.62  
   34.63 @@ -92,7 +92,7 @@
   34.64    done
   34.65  
   34.66  lemma ntree_univ: "ntree(univ(A)) \<subseteq> univ(A)"
   34.67 -  -- \<open>Easily provable by induction also\<close>
   34.68 +  \<comment> \<open>Easily provable by induction also\<close>
   34.69    apply (unfold ntree.defs ntree.con_defs)
   34.70    apply (rule lfp_lowerbound)
   34.71     apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   34.72 @@ -104,7 +104,7 @@
   34.73  
   34.74  
   34.75  text \<open>
   34.76 -  \medskip @{text ntree} recursion.
   34.77 +  \medskip \<open>ntree\<close> recursion.
   34.78  \<close>
   34.79  
   34.80  lemma ntree_rec_Branch:
   34.81 @@ -125,7 +125,7 @@
   34.82  
   34.83  
   34.84  text \<open>
   34.85 -  \medskip @{text maptree}
   34.86 +  \medskip \<open>maptree\<close>
   34.87  \<close>
   34.88  
   34.89  lemma maptree_unfold: "maptree(A) = A \<times> (maptree(A) -||> maptree(A))"
   34.90 @@ -138,7 +138,7 @@
   34.91                    \<forall>y \<in> field(h). P(y)
   34.92                 |] ==> P(Sons(x,h))"
   34.93    shows "P(t)"
   34.94 -  -- \<open>A nicer induction rule than the standard one.\<close>
   34.95 +  \<comment> \<open>A nicer induction rule than the standard one.\<close>
   34.96    using t
   34.97    apply induct
   34.98    apply (assumption | rule step)+
   34.99 @@ -150,7 +150,7 @@
  34.100  
  34.101  
  34.102  text \<open>
  34.103 -  \medskip @{text maptree2}
  34.104 +  \medskip \<open>maptree2\<close>
  34.105  \<close>
  34.106  
  34.107  lemma maptree2_unfold: "maptree2(A, B) = A \<times> (B -||> maptree2(A, B))"
    35.1 --- a/src/ZF/Induct/Primrec.thy	Mon Dec 07 10:19:30 2015 +0100
    35.2 +++ b/src/ZF/Induct/Primrec.thy	Mon Dec 07 10:23:50 2015 +0100
    35.3 @@ -37,7 +37,7 @@
    35.4    "PREC(f,g) ==
    35.5       \<lambda>l \<in> list(nat). list_case(0,
    35.6                        \<lambda>x xs. rec(x, f`xs, \<lambda>y r. g ` Cons(r, Cons(y, xs))), l)"
    35.7 -  -- \<open>Note that @{text g} is applied first to @{term "PREC(f,g)`y"} and then to @{text y}!\<close>
    35.8 +  \<comment> \<open>Note that \<open>g\<close> is applied first to @{term "PREC(f,g)`y"} and then to \<open>y\<close>!\<close>
    35.9  
   35.10  consts
   35.11    ACK :: "i=>i"
   35.12 @@ -115,16 +115,16 @@
   35.13  subsection \<open>Ackermann's function cases\<close>
   35.14  
   35.15  lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"
   35.16 -  -- \<open>PROPERTY A 1\<close>
   35.17 +  \<comment> \<open>PROPERTY A 1\<close>
   35.18    by (simp add: SC)
   35.19  
   35.20  lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
   35.21 -  -- \<open>PROPERTY A 2\<close>
   35.22 +  \<comment> \<open>PROPERTY A 2\<close>
   35.23    by (simp add: CONSTANT PREC_0)
   35.24  
   35.25  lemma ack_succ_succ:
   35.26    "[| i\<in>nat;  j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
   35.27 -  -- \<open>PROPERTY A 3\<close>
   35.28 +  \<comment> \<open>PROPERTY A 3\<close>
   35.29    by (simp add: CONSTANT PREC_succ COMP_1 PROJ_0)
   35.30  
   35.31  lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type
   35.32 @@ -132,7 +132,7 @@
   35.33  
   35.34  
   35.35  lemma lt_ack2: "i \<in> nat ==> j \<in> nat ==> j < ack(i,j)"
   35.36 -  -- \<open>PROPERTY A 4\<close>
   35.37 +  \<comment> \<open>PROPERTY A 4\<close>
   35.38    apply (induct i arbitrary: j set: nat)
   35.39     apply simp
   35.40    apply (induct_tac j)
   35.41 @@ -142,11 +142,11 @@
   35.42    done
   35.43  
   35.44  lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"
   35.45 -  -- \<open>PROPERTY A 5-, the single-step lemma\<close>
   35.46 +  \<comment> \<open>PROPERTY A 5-, the single-step lemma\<close>
   35.47    by (induct set: nat) (simp_all add: lt_ack2)
   35.48  
   35.49  lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"
   35.50 -  -- \<open>PROPERTY A 5, monotonicity for @{text "<"}\<close>
   35.51 +  \<comment> \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close>
   35.52    apply (frule lt_nat_in_nat, assumption)
   35.53    apply (erule succ_lt_induct)
   35.54      apply assumption
   35.55 @@ -155,14 +155,14 @@
   35.56    done
   35.57  
   35.58  lemma ack_le_mono2: "[|j\<le>k;  i\<in>nat;  k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)"
   35.59 -  -- \<open>PROPERTY A 5', monotonicity for @{text \<le>}\<close>
   35.60 +  \<comment> \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close>
   35.61    apply (rule_tac f = "\<lambda>j. ack (i,j) " in Ord_lt_mono_imp_le_mono)
   35.62       apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+
   35.63    done
   35.64  
   35.65  lemma ack2_le_ack1:
   35.66    "[| i\<in>nat;  j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"
   35.67 -  -- \<open>PROPERTY A 6\<close>
   35.68 +  \<comment> \<open>PROPERTY A 6\<close>
   35.69    apply (induct_tac j)
   35.70     apply simp_all
   35.71    apply (rule ack_le_mono2)
   35.72 @@ -171,14 +171,14 @@
   35.73    done
   35.74  
   35.75  lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)"
   35.76 -  -- \<open>PROPERTY A 7-, the single-step lemma\<close>
   35.77 +  \<comment> \<open>PROPERTY A 7-, the single-step lemma\<close>
   35.78    apply (rule ack_lt_mono2 [THEN lt_trans2])
   35.79       apply (rule_tac [4] ack2_le_ack1)
   35.80        apply auto
   35.81    done
   35.82  
   35.83  lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)"
   35.84 -  -- \<open>PROPERTY A 7, monotonicity for @{text "<"}\<close>
   35.85 +  \<comment> \<open>PROPERTY A 7, monotonicity for \<open><\<close>\<close>
   35.86    apply (frule lt_nat_in_nat, assumption)
   35.87    apply (erule succ_lt_induct)
   35.88      apply assumption
   35.89 @@ -187,23 +187,23 @@
   35.90    done
   35.91  
   35.92  lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)"
   35.93 -  -- \<open>PROPERTY A 7', monotonicity for @{text \<le>}\<close>
   35.94 +  \<comment> \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close>
   35.95    apply (rule_tac f = "\<lambda>j. ack (j,k) " in Ord_lt_mono_imp_le_mono)
   35.96       apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+
   35.97    done
   35.98  
   35.99  lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"
  35.100 -  -- \<open>PROPERTY A 8\<close>
  35.101 +  \<comment> \<open>PROPERTY A 8\<close>
  35.102    by (induct set: nat) simp_all
  35.103  
  35.104  lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
  35.105 -  -- \<open>PROPERTY A 9\<close>
  35.106 +  \<comment> \<open>PROPERTY A 9\<close>
  35.107    by (induct set: nat) (simp_all add: ack_1)
  35.108  
  35.109  lemma ack_nest_bound:
  35.110    "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
  35.111      ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
  35.112 -  -- \<open>PROPERTY A 10\<close>
  35.113 +  \<comment> \<open>PROPERTY A 10\<close>
  35.114    apply (rule lt_trans2 [OF _ ack2_le_ack1])
  35.115      apply simp
  35.116      apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
  35.117 @@ -214,7 +214,7 @@
  35.118  lemma ack_add_bound:
  35.119    "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
  35.120      ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
  35.121 -  -- \<open>PROPERTY A 11\<close>
  35.122 +  \<comment> \<open>PROPERTY A 11\<close>
  35.123    apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans)
  35.124     apply (simp add: ack_2)
  35.125     apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
  35.126 @@ -225,9 +225,9 @@
  35.127  lemma ack_add_bound2:
  35.128       "[| i < ack(k,j);  j \<in> nat;  k \<in> nat |]
  35.129        ==> i#+j < ack(succ(succ(succ(succ(k)))), j)"
  35.130 -  -- \<open>PROPERTY A 12.\<close>
  35.131 -  -- \<open>Article uses existential quantifier but the ALF proof used @{term "k#+#4"}.\<close>
  35.132 -  -- \<open>Quantified version must be nested @{text "\<exists>k'. \<forall>i,j \<dots>"}.\<close>
  35.133 +  \<comment> \<open>PROPERTY A 12.\<close>
  35.134 +  \<comment> \<open>Article uses existential quantifier but the ALF proof used @{term "k#+#4"}.\<close>
  35.135 +  \<comment> \<open>Quantified version must be nested \<open>\<exists>k'. \<forall>i,j \<dots>\<close>.\<close>
  35.136    apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
  35.137     apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
  35.138        apply (rule add_lt_mono)
  35.139 @@ -247,7 +247,7 @@
  35.140    done
  35.141  
  35.142  lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
  35.143 -  -- \<open>PROPERTY A 4'? Extra lemma needed for @{text CONSTANT} case, constant functions.\<close>
  35.144 +  \<comment> \<open>PROPERTY A 4'? Extra lemma needed for \<open>CONSTANT\<close> case, constant functions.\<close>
  35.145    apply (induct_tac i)
  35.146     apply (simp add: nat_0_le)
  35.147    apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
  35.148 @@ -275,7 +275,7 @@
  35.149    done
  35.150  
  35.151  text \<open>
  35.152 -  \medskip @{text COMP} case.
  35.153 +  \medskip \<open>COMP\<close> case.
  35.154  \<close>
  35.155  
  35.156  lemma COMP_map_lemma:
  35.157 @@ -312,7 +312,7 @@
  35.158    done
  35.159  
  35.160  text \<open>
  35.161 -  \medskip @{text PREC} case.
  35.162 +  \medskip \<open>PREC\<close> case.
  35.163  \<close>
  35.164  
  35.165  lemma PREC_case_lemma:
  35.166 @@ -326,7 +326,7 @@
  35.167    apply (erule list.cases)
  35.168     apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
  35.169    apply simp
  35.170 -  apply (erule ssubst)  -- \<open>get rid of the needless assumption\<close>
  35.171 +  apply (erule ssubst)  \<comment> \<open>get rid of the needless assumption\<close>
  35.172    apply (induct_tac a)
  35.173     apply simp_all
  35.174     txt \<open>base case\<close>
    36.1 --- a/src/ZF/Induct/PropLog.thy	Mon Dec 07 10:19:30 2015 +0100
    36.2 +++ b/src/ZF/Induct/PropLog.thy	Mon Dec 07 10:23:50 2015 +0100
    36.3 @@ -14,8 +14,8 @@
    36.4    Inductive definition of propositional logic.  Soundness and
    36.5    completeness w.r.t.\ truth-tables.
    36.6  
    36.7 -  Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
    36.8 -  Fin(H)"}
    36.9 +  Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in>
   36.10 +  Fin(H)\<close>
   36.11  \<close>
   36.12  
   36.13  
   36.14 @@ -66,7 +66,7 @@
   36.15  definition
   36.16    is_true :: "[i,i] => o"  where
   36.17    "is_true(p,t) == is_true_fun(p,t) = 1"
   36.18 -  -- \<open>this definition is required since predicates can't be recursive\<close>
   36.19 +  \<comment> \<open>this definition is required since predicates can't be recursive\<close>
   36.20  
   36.21  lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
   36.22    by (simp add: is_true_def)
   36.23 @@ -81,8 +81,8 @@
   36.24  subsubsection \<open>Logical consequence\<close>
   36.25  
   36.26  text \<open>
   36.27 -  For every valuation, if all elements of @{text H} are true then so
   36.28 -  is @{text p}.
   36.29 +  For every valuation, if all elements of \<open>H\<close> are true then so
   36.30 +  is \<open>p\<close>.
   36.31  \<close>
   36.32  
   36.33  definition
   36.34 @@ -91,8 +91,8 @@
   36.35  
   36.36  
   36.37  text \<open>
   36.38 -  A finite set of hypotheses from @{text t} and the @{text Var}s in
   36.39 -  @{text p}.
   36.40 +  A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in
   36.41 +  \<open>p\<close>.
   36.42  \<close>
   36.43  
   36.44  consts
   36.45 @@ -118,13 +118,13 @@
   36.46  inductive_cases ImpE: "p=>q \<in> propn"
   36.47  
   36.48  lemma thms_MP: "[| H |- p=>q;  H |- p |] ==> H |- q"
   36.49 -  -- \<open>Stronger Modus Ponens rule: no typechecking!\<close>
   36.50 +  \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close>
   36.51    apply (rule thms.MP)
   36.52       apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
   36.53    done
   36.54  
   36.55  lemma thms_I: "p \<in> propn ==> H |- p=>p"
   36.56 -  -- \<open>Rule is called @{text I} for Identity Combinator, not for Introduction.\<close>
   36.57 +  \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
   36.58    apply (rule thms.S [THEN thms_MP, THEN thms_MP])
   36.59        apply (rule_tac [5] thms.K)
   36.60         apply (rule_tac [4] thms.K)
   36.61 @@ -135,7 +135,7 @@
   36.62  subsubsection \<open>Weakening, left and right\<close>
   36.63  
   36.64  lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
   36.65 -  -- \<open>Order of premises is convenient with @{text THEN}\<close>
   36.66 +  \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close>
   36.67    by (erule thms_mono [THEN subsetD])
   36.68  
   36.69  lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
   36.70 @@ -208,7 +208,7 @@
   36.71  
   36.72  lemma hyps_thms_if:
   36.73      "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
   36.74 -  -- \<open>Typical example of strengthening the induction statement.\<close>
   36.75 +  \<comment> \<open>Typical example of strengthening the induction statement.\<close>
   36.76    apply simp
   36.77    apply (induct_tac p)
   36.78      apply (simp_all add: thms_I thms.H)
   36.79 @@ -217,7 +217,7 @@
   36.80    done
   36.81  
   36.82  lemma logcon_thms_p: "[| p \<in> propn;  0 |= p |] ==> hyps(p,t) |- p"
   36.83 -  -- \<open>Key lemma for completeness; yields a set of assumptions satisfying @{text p}\<close>
   36.84 +  \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close>
   36.85    apply (drule hyps_thms_if)
   36.86    apply (simp add: logcon_def)
   36.87    done
   36.88 @@ -242,7 +242,7 @@
   36.89  
   36.90  lemma thms_excluded_middle_rule:
   36.91    "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \<in> propn |] ==> H |- q"
   36.92 -  -- \<open>Hard to prove directly because it requires cuts\<close>
   36.93 +  \<comment> \<open>Hard to prove directly because it requires cuts\<close>
   36.94    apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
   36.95       apply (blast intro!: propn_SIs intro: propn_Is)+
   36.96    done
   36.97 @@ -268,7 +268,7 @@
   36.98      "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
   36.99    by (induct set: propn) auto
  36.100  
  36.101 -text \<open>Two lemmas for use with @{text weaken_left}\<close>
  36.102 +text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close>
  36.103  
  36.104  lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
  36.105    by blast
  36.106 @@ -317,13 +317,13 @@
  36.107  subsubsection \<open>Completeness theorem\<close>
  36.108  
  36.109  lemma completeness_0: "[| p \<in> propn;  0 |= p |] ==> 0 |- p"
  36.110 -  -- \<open>The base case for completeness\<close>
  36.111 +  \<comment> \<open>The base case for completeness\<close>
  36.112    apply (rule Diff_cancel [THEN subst])
  36.113    apply (blast intro: completeness_0_lemma)
  36.114    done
  36.115  
  36.116  lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
  36.117 -  -- \<open>A semantic analogue of the Deduction Theorem\<close>
  36.118 +  \<comment> \<open>A semantic analogue of the Deduction Theorem\<close>
  36.119    by (simp add: logcon_def)
  36.120  
  36.121  lemma completeness:
    37.1 --- a/src/ZF/Induct/Rmap.thy	Mon Dec 07 10:19:30 2015 +0100
    37.2 +++ b/src/ZF/Induct/Rmap.thy	Mon Dec 07 10:23:50 2015 +0100
    37.3 @@ -53,7 +53,7 @@
    37.4    done
    37.5  
    37.6  text \<open>
    37.7 -  \medskip If @{text f} is a function then @{text "rmap(f)"} behaves
    37.8 +  \medskip If \<open>f\<close> is a function then \<open>rmap(f)\<close> behaves
    37.9    as expected.
   37.10  \<close>
   37.11  
    38.1 --- a/src/ZF/Induct/Term.thy	Mon Dec 07 10:19:30 2015 +0100
    38.2 +++ b/src/ZF/Induct/Term.thy	Mon Dec 07 10:23:50 2015 +0100
    38.3 @@ -8,8 +8,7 @@
    38.4  theory Term imports Main begin
    38.5  
    38.6  text \<open>
    38.7 -  Illustrates the list functor (essentially the same type as in @{text
    38.8 -  Trees_Forest}).
    38.9 +  Illustrates the list functor (essentially the same type as in \<open>Trees_Forest\<close>).
   38.10  \<close>
   38.11  
   38.12  consts
   38.13 @@ -56,7 +55,7 @@
   38.14        !!x z zs. [| x \<in> A;  z \<in> term(A);  zs: list(term(A));  P(Apply(x,zs))
   38.15                  |] ==> P(Apply(x, Cons(z,zs)))
   38.16       |] ==> P(t)"
   38.17 -  -- \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
   38.18 +  \<comment> \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
   38.19    apply (induct_tac t)
   38.20    apply (erule list.induct)
   38.21     apply (auto dest: list_CollectD)
   38.22 @@ -67,7 +66,7 @@
   38.23        !!x zs. [| x \<in> A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==>
   38.24                f(Apply(x,zs)) = g(Apply(x,zs))
   38.25     |] ==> f(t) = g(t)"
   38.26 -  -- \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
   38.27 +  \<comment> \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
   38.28    apply (induct_tac t)
   38.29    apply (auto dest: map_list_Collect list_CollectD)
   38.30    done
   38.31 @@ -85,7 +84,7 @@
   38.32    done
   38.33  
   38.34  lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
   38.35 -  -- \<open>Easily provable by induction also\<close>
   38.36 +  \<comment> \<open>Easily provable by induction also\<close>
   38.37    apply (unfold term.defs term.con_defs)
   38.38    apply (rule lfp_lowerbound)
   38.39     apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   38.40 @@ -103,12 +102,12 @@
   38.41    by (rule term_subset_univ [THEN subsetD])
   38.42  
   38.43  text \<open>
   38.44 -  \medskip @{text term_rec} -- by @{text Vset} recursion.
   38.45 +  \medskip \<open>term_rec\<close> -- by \<open>Vset\<close> recursion.
   38.46  \<close>
   38.47  
   38.48  lemma map_lemma: "[| l \<in> list(A);  Ord(i);  rank(l)<i |]
   38.49      ==> map(\<lambda>z. (\<lambda>x \<in> Vset(i).h(x)) ` z, l) = map(h,l)"
   38.50 -  -- \<open>@{term map} works correctly on the underlying list of terms.\<close>
   38.51 +  \<comment> \<open>@{term map} works correctly on the underlying list of terms.\<close>
   38.52    apply (induct set: list)
   38.53     apply simp
   38.54    apply (subgoal_tac "rank (a) <i & rank (l) < i")
   38.55 @@ -119,7 +118,7 @@
   38.56  
   38.57  lemma term_rec [simp]: "ts \<in> list(A) ==>
   38.58    term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))"
   38.59 -  -- \<open>Typing premise is necessary to invoke @{text map_lemma}.\<close>
   38.60 +  \<comment> \<open>Typing premise is necessary to invoke \<open>map_lemma\<close>.\<close>
   38.61    apply (rule term_rec_def [THEN def_Vrec, THEN trans])
   38.62    apply (unfold term.con_defs)
   38.63    apply (simp add: rank_pair2 map_lemma)
   38.64 @@ -131,7 +130,7 @@
   38.65                     r \<in> list(\<Union>t \<in> term(A). C(t)) |]
   38.66                  ==> d(x, zs, r): C(Apply(x,zs))"
   38.67    shows "term_rec(t,d) \<in> C(t)"
   38.68 -  -- \<open>Slightly odd typing condition on @{text r} in the second premise!\<close>
   38.69 +  \<comment> \<open>Slightly odd typing condition on \<open>r\<close> in the second premise!\<close>
   38.70    using t
   38.71    apply induct
   38.72    apply (frule list_CollectD)
   38.73 @@ -194,7 +193,7 @@
   38.74  
   38.75  
   38.76  text \<open>
   38.77 -  \medskip @{text reflect}.
   38.78 +  \medskip \<open>reflect\<close>.
   38.79  \<close>
   38.80  
   38.81  lemma reflect [simp]:
   38.82 @@ -206,7 +205,7 @@
   38.83  
   38.84  
   38.85  text \<open>
   38.86 -  \medskip @{text preorder}.
   38.87 +  \medskip \<open>preorder\<close>.
   38.88  \<close>
   38.89  
   38.90  lemma preorder [simp]:
   38.91 @@ -218,7 +217,7 @@
   38.92  
   38.93  
   38.94  text \<open>
   38.95 -  \medskip @{text postorder}.
   38.96 +  \medskip \<open>postorder\<close>.
   38.97  \<close>
   38.98  
   38.99  lemma postorder [simp]:
  38.100 @@ -230,7 +229,7 @@
  38.101  
  38.102  
  38.103  text \<open>
  38.104 -  \medskip Theorems about @{text term_map}.
  38.105 +  \medskip Theorems about \<open>term_map\<close>.
  38.106  \<close>
  38.107  
  38.108  declare map_compose [simp]
  38.109 @@ -248,7 +247,7 @@
  38.110  
  38.111  
  38.112  text \<open>
  38.113 -  \medskip Theorems about @{text term_size}.
  38.114 +  \medskip Theorems about \<open>term_size\<close>.
  38.115  \<close>
  38.116  
  38.117  lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"
  38.118 @@ -262,7 +261,7 @@
  38.119  
  38.120  
  38.121  text \<open>
  38.122 -  \medskip Theorems about @{text reflect}.
  38.123 +  \medskip Theorems about \<open>reflect\<close>.
  38.124  \<close>
  38.125  
  38.126  lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t"
    39.1 --- a/src/ZF/Induct/Tree_Forest.thy	Mon Dec 07 10:19:30 2015 +0100
    39.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Mon Dec 07 10:23:50 2015 +0100
    39.3 @@ -61,7 +61,7 @@
    39.4  
    39.5  lemma tree_forest_unfold:
    39.6    "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
    39.7 -    -- \<open>NOT useful, but interesting \dots\<close>
    39.8 +    \<comment> \<open>NOT useful, but interesting \dots\<close>
    39.9    supply rews = tree_forest.con_defs tree_def forest_def
   39.10    apply (unfold tree_def forest_def)
   39.11    apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
   39.12 @@ -108,7 +108,7 @@
   39.13                      |] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f))
   39.14     |] ==> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
   39.15            (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
   39.16 -    -- \<open>Mutually recursive version.\<close>
   39.17 +    \<comment> \<open>Mutually recursive version.\<close>
   39.18    apply (unfold Ball_def)
   39.19    apply (rule tree_forest.mutual_induct)
   39.20    apply simp_all
   39.21 @@ -157,7 +157,7 @@
   39.22  
   39.23  
   39.24  text \<open>
   39.25 -  \medskip @{text list_of_TF} and @{text of_list}.
   39.26 +  \medskip \<open>list_of_TF\<close> and \<open>of_list\<close>.
   39.27  \<close>
   39.28  
   39.29  lemma list_of_TF_type [TC]:
   39.30 @@ -168,7 +168,7 @@
   39.31    by (induct set: list) simp_all
   39.32  
   39.33  text \<open>
   39.34 -  \medskip @{text map}.
   39.35 +  \medskip \<open>map\<close>.
   39.36  \<close>
   39.37  
   39.38  lemma
   39.39 @@ -179,7 +179,7 @@
   39.40    by (induct rule: tree'induct forest'induct) simp_all
   39.41  
   39.42  text \<open>
   39.43 -  \medskip @{text size}.
   39.44 +  \medskip \<open>size\<close>.
   39.45  \<close>
   39.46  
   39.47  lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
   39.48 @@ -187,7 +187,7 @@
   39.49  
   39.50  
   39.51  text \<open>
   39.52 -  \medskip @{text preorder}.
   39.53 +  \medskip \<open>preorder\<close>.
   39.54  \<close>
   39.55  
   39.56  lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
   39.57 @@ -195,7 +195,7 @@
   39.58  
   39.59  
   39.60  text \<open>
   39.61 -  \medskip Theorems about @{text list_of_TF} and @{text of_list}.
   39.62 +  \medskip Theorems about \<open>list_of_TF\<close> and \<open>of_list\<close>.
   39.63  \<close>
   39.64  
   39.65  lemma forest_induct [consumes 1, case_names Fnil Fcons]:
   39.66 @@ -203,7 +203,7 @@
   39.67        R(Fnil);
   39.68        !!t f. [| t \<in> tree(A);  f \<in> forest(A);  R(f) |] ==> R(Fcons(t,f))
   39.69     |] ==> R(f)"
   39.70 -  -- \<open>Essentially the same as list induction.\<close>
   39.71 +  \<comment> \<open>Essentially the same as list induction.\<close>
   39.72    apply (erule tree_forest.mutual_induct
   39.73        [THEN conjunct2, THEN spec, THEN [2] rev_mp])
   39.74      apply (rule TrueI)
   39.75 @@ -219,7 +219,7 @@
   39.76  
   39.77  
   39.78  text \<open>
   39.79 -  \medskip Theorems about @{text map}.
   39.80 +  \medskip Theorems about \<open>map\<close>.
   39.81  \<close>
   39.82  
   39.83  lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
   39.84 @@ -231,7 +231,7 @@
   39.85  
   39.86  
   39.87  text \<open>
   39.88 -  \medskip Theorems about @{text size}.
   39.89 +  \medskip Theorems about \<open>size\<close>.
   39.90  \<close>
   39.91  
   39.92  lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
   39.93 @@ -241,7 +241,7 @@
   39.94    by (induct set: tree_forest) (simp_all add: length_app)
   39.95  
   39.96  text \<open>
   39.97 -  \medskip Theorems about @{text preorder}.
   39.98 +  \medskip Theorems about \<open>preorder\<close>.
   39.99  \<close>
  39.100  
  39.101  lemma preorder_map:
    40.1 --- a/src/ZF/InfDatatype.thy	Mon Dec 07 10:19:30 2015 +0100
    40.2 +++ b/src/ZF/InfDatatype.thy	Mon Dec 07 10:23:50 2015 +0100
    40.3 @@ -70,7 +70,7 @@
    40.4         ==> f: Vfrom(A,csucc(K))"
    40.5  by (blast intro: fun_Vcsucc [THEN subsetD])
    40.6  
    40.7 -text\<open>Remove @{text "\<subseteq>"} from the rule above\<close>
    40.8 +text\<open>Remove \<open>\<subseteq>\<close> from the rule above\<close>
    40.9  lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]
   40.10  
   40.11  (** Version where K itself is the index set **)
    41.1 --- a/src/ZF/IntDiv_ZF.thy	Mon Dec 07 10:19:30 2015 +0100
    41.2 +++ b/src/ZF/IntDiv_ZF.thy	Mon Dec 07 10:23:50 2015 +0100
    41.3 @@ -401,7 +401,7 @@
    41.4  
    41.5  
    41.6  subsection\<open>Correctness of posDivAlg,
    41.7 -           the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"}\<close>
    41.8 +           the Division Algorithm for \<open>a\<ge>0\<close> and \<open>b>0\<close>\<close>
    41.9  
   41.10  lemma adjust_eq [simp]:
   41.11       "adjust(b, <q,r>) = (let diff = r$-b in
    42.1 --- a/src/ZF/Int_ZF.thy	Mon Dec 07 10:19:30 2015 +0100
    42.2 +++ b/src/ZF/Int_ZF.thy	Mon Dec 07 10:23:50 2015 +0100
    42.3 @@ -17,11 +17,11 @@
    42.4      "int == (nat*nat)//intrel"
    42.5  
    42.6  definition
    42.7 -  int_of :: "i=>i" --\<open>coercion from nat to int\<close>    ("$# _" [80] 80)  where
    42.8 +  int_of :: "i=>i" \<comment>\<open>coercion from nat to int\<close>    ("$# _" [80] 80)  where
    42.9      "$# m == intrel `` {<natify(m), 0>}"
   42.10  
   42.11  definition
   42.12 -  intify :: "i=>i" --\<open>coercion from ANYTHING to int\<close>  where
   42.13 +  intify :: "i=>i" \<comment>\<open>coercion from ANYTHING to int\<close>  where
   42.14      "intify(m) == if m \<in> int then m else $#0"
   42.15  
   42.16  definition
   42.17 @@ -50,7 +50,7 @@
   42.18  
   42.19  definition
   42.20    zmagnitude  ::      "i=>i"  where
   42.21 -  --\<open>could be replaced by an absolute value function from int to int?\<close>
   42.22 +  \<comment>\<open>could be replaced by an absolute value function from int to int?\<close>
   42.23      "zmagnitude(z) ==
   42.24       THE m. m\<in>nat & ((~ znegative(z) & z = $# m) |
   42.25                         (znegative(z) & $- z = $# m))"
   42.26 @@ -770,7 +770,7 @@
   42.27  by (simp add: not_zless_iff_zle [THEN iff_sym])
   42.28  
   42.29  
   42.30 -subsection\<open>More subtraction laws (for @{text zcompare_rls})\<close>
   42.31 +subsection\<open>More subtraction laws (for \<open>zcompare_rls\<close>)\<close>
   42.32  
   42.33  lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
   42.34  by (simp add: zdiff_def zadd_ac)
   42.35 @@ -808,7 +808,7 @@
   42.36  
   42.37  text\<open>This list of rewrites simplifies (in)equalities by bringing subtractions
   42.38    to the top and then moving negative terms to the other side.
   42.39 -  Use with @{text zadd_ac}\<close>
   42.40 +  Use with \<open>zadd_ac\<close>\<close>
   42.41  lemmas zcompare_rls =
   42.42       zdiff_def [symmetric]
   42.43       zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2
    43.1 --- a/src/ZF/List_ZF.thy	Mon Dec 07 10:19:30 2015 +0100
    43.2 +++ b/src/ZF/List_ZF.thy	Mon Dec 07 10:23:50 2015 +0100
    43.3 @@ -98,7 +98,7 @@
    43.4  
    43.5  definition
    43.6    nth :: "[i, i]=>i"  where
    43.7 -  --\<open>returns the (n+1)th element of a list, or 0 if the
    43.8 +  \<comment>\<open>returns the (n+1)th element of a list, or 0 if the
    43.9     list is too short.\<close>
   43.10    "nth(n, as) == list_rec(\<lambda>n\<in>nat. 0,
   43.11                            %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
    44.1 --- a/src/ZF/Order.thy	Mon Dec 07 10:19:30 2015 +0100
    44.2 +++ b/src/ZF/Order.thy	Mon Dec 07 10:23:50 2015 +0100
    44.3 @@ -11,8 +11,8 @@
    44.4  
    44.5  theory Order imports WF Perm begin
    44.6  
    44.7 -text \<open>We adopt the following convention: @{text ord} is used for
    44.8 -  strict orders and @{text order} is used for their reflexive
    44.9 +text \<open>We adopt the following convention: \<open>ord\<close> is used for
   44.10 +  strict orders and \<open>order\<close> is used for their reflexive
   44.11    counterparts.\<close>
   44.12  
   44.13  definition
    45.1 --- a/src/ZF/OrderArith.thy	Mon Dec 07 10:19:30 2015 +0100
    45.2 +++ b/src/ZF/OrderArith.thy	Mon Dec 07 10:23:50 2015 +0100
    45.3 @@ -87,7 +87,7 @@
    45.4  lemma wf_on_radd: "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
    45.5  apply (rule wf_onI2)
    45.6  apply (subgoal_tac "\<forall>x\<in>A. Inl (x) \<in> Ba")
    45.7 - --\<open>Proving the lemma, which is needed twice!\<close>
    45.8 + \<comment>\<open>Proving the lemma, which is needed twice!\<close>
    45.9   prefer 2
   45.10   apply (erule_tac V = "y \<in> A + B" in thin_rl)
   45.11   apply (rule_tac ballI)
   45.12 @@ -369,8 +369,8 @@
   45.13  apply blast
   45.14  done
   45.15  
   45.16 -text\<open>But note that the combination of @{text wf_imp_wf_on} and
   45.17 - @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
   45.18 +text\<open>But note that the combination of \<open>wf_imp_wf_on\<close> and
   45.19 + \<open>wf_rvimage\<close> gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
   45.20  lemma wf_on_rvimage: "[| f \<in> A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
   45.21  apply (rule wf_onI2)
   45.22  apply (subgoal_tac "\<forall>z\<in>A. f`z=f`y \<longrightarrow> z \<in> Ba")
   45.23 @@ -460,7 +460,7 @@
   45.24  lemma wf_times: "A \<inter> B = 0 ==> wf(A*B)"
   45.25  by (simp add: wf_def, blast)
   45.26  
   45.27 -text\<open>Could also be used to prove @{text wf_radd}\<close>
   45.28 +text\<open>Could also be used to prove \<open>wf_radd\<close>\<close>
   45.29  lemma wf_Un:
   45.30       "[| range(r) \<inter> domain(s) = 0; wf(r);  wf(s) |] ==> wf(r \<union> s)"
   45.31  apply (simp add: wf_def, clarify)
    46.1 --- a/src/ZF/Ordinal.thy	Mon Dec 07 10:19:30 2015 +0100
    46.2 +++ b/src/ZF/Ordinal.thy	Mon Dec 07 10:23:50 2015 +0100
    46.3 @@ -390,7 +390,7 @@
    46.4  by (rule_tac i = i and j = j in Ord_linear2, auto)
    46.5  
    46.6  
    46.7 -subsubsection \<open>Some Rewrite Rules for @{text "<"}, @{text "\<le>"}\<close>
    46.8 +subsubsection \<open>Some Rewrite Rules for \<open><\<close>, \<open>\<le>\<close>\<close>
    46.9  
   46.10  lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
   46.11  by (unfold lt_def, blast)
    47.1 --- a/src/ZF/UNITY/AllocBase.thy	Mon Dec 07 10:19:30 2015 +0100
    47.2 +++ b/src/ZF/UNITY/AllocBase.thy	Mon Dec 07 10:23:50 2015 +0100
    47.3 @@ -45,11 +45,11 @@
    47.4     "all_distinct(l) == all_distinct0(l)=1"
    47.5    
    47.6  definition  
    47.7 -  state_of :: "i =>i" --\<open>coersion from anyting to state\<close>  where
    47.8 +  state_of :: "i =>i" \<comment>\<open>coersion from anyting to state\<close>  where
    47.9     "state_of(s) == if s \<in> state then s else st0"
   47.10  
   47.11  definition
   47.12 -  lift :: "i =>(i=>i)" --\<open>simplifies the expression of programs\<close>  where
   47.13 +  lift :: "i =>(i=>i)" \<comment>\<open>simplifies the expression of programs\<close>  where
   47.14     "lift(x) == %s. s`x"
   47.15  
   47.16  text\<open>function to show that the set of variables is infinite\<close>
    48.1 --- a/src/ZF/UNITY/Distributor.thy	Mon Dec 07 10:19:30 2015 +0100
    48.2 +++ b/src/ZF/UNITY/Distributor.thy	Mon Dec 07 10:23:50 2015 +0100
    48.3 @@ -37,10 +37,10 @@
    48.4       distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)"
    48.5  
    48.6  locale distr =
    48.7 -  fixes In  --\<open>items to distribute\<close>
    48.8 -    and iIn --\<open>destinations of items to distribute\<close>
    48.9 -    and Out --\<open>distributed items\<close>
   48.10 -    and A   --\<open>the type of items being distributed\<close>
   48.11 +  fixes In  \<comment>\<open>items to distribute\<close>
   48.12 +    and iIn \<comment>\<open>destinations of items to distribute\<close>
   48.13 +    and Out \<comment>\<open>distributed items\<close>
   48.14 +    and A   \<comment>\<open>the type of items being distributed\<close>
   48.15      and D
   48.16   assumes
   48.17       var_assumes [simp]:  "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)"
    49.1 --- a/src/ZF/UNITY/Merge.thy	Mon Dec 07 10:19:30 2015 +0100
    49.2 +++ b/src/ZF/UNITY/Merge.thy	Mon Dec 07 10:23:50 2015 +0100
    49.3 @@ -64,10 +64,10 @@
    49.4  
    49.5  (** State definitions.  OUTPUT variables are locals **)
    49.6  locale merge =
    49.7 -  fixes In   --\<open>merge's INPUT histories: streams to merge\<close>
    49.8 -    and Out  --\<open>merge's OUTPUT history: merged items\<close>
    49.9 -    and iOut --\<open>merge's OUTPUT history: origins of merged items\<close>
   49.10 -    and A    --\<open>the type of items being merged\<close>
   49.11 +  fixes In   \<comment>\<open>merge's INPUT histories: streams to merge\<close>
   49.12 +    and Out  \<comment>\<open>merge's OUTPUT history: merged items\<close>
   49.13 +    and iOut \<comment>\<open>merge's OUTPUT history: origins of merged items\<close>
   49.14 +    and A    \<comment>\<open>the type of items being merged\<close>
   49.15      and M
   49.16   assumes var_assumes [simp]:
   49.17             "(\<forall>n. In(n):var) & Out \<in> var & iOut \<in> var"
    50.1 --- a/src/ZF/UNITY/Mutex.thy	Mon Dec 07 10:19:30 2015 +0100
    50.2 +++ b/src/ZF/UNITY/Mutex.thy	Mon Dec 07 10:23:50 2015 +0100
    50.3 @@ -27,7 +27,7 @@
    50.4  abbreviation "u == Var([0,1])"
    50.5  abbreviation "v == Var([1,0])"
    50.6  
    50.7 -axiomatization where --\<open>* Type declarations  *\<close>
    50.8 +axiomatization where \<comment>\<open>* Type declarations  *\<close>
    50.9    p_type:  "type_of(p)=bool & default_val(p)=0" and
   50.10    m_type:  "type_of(m)=int  & default_val(m)=#0" and
   50.11    n_type:  "type_of(n)=int  & default_val(n)=#0" and
    51.1 --- a/src/ZF/UNITY/UNITY.thy	Mon Dec 07 10:19:30 2015 +0100
    51.2 +++ b/src/ZF/UNITY/UNITY.thy	Mon Dec 07 10:23:50 2015 +0100
    51.3 @@ -20,7 +20,7 @@
    51.4  
    51.5  definition
    51.6    mk_program :: "[i,i,i]=>i"  where
    51.7 -  --\<open>The definition yields a program thanks to the coercions
    51.8 +  \<comment>\<open>The definition yields a program thanks to the coercions
    51.9         init \<inter> state, acts \<inter> Pow(state*state), etc.\<close>
   51.10    "mk_program(init, acts, allowed) ==
   51.11      <init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)),
   51.12 @@ -70,7 +70,7 @@
   51.13  
   51.14  definition "constrains" :: "[i, i] => i"  (infixl "co" 60)  where
   51.15    "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
   51.16 -    --\<open>the condition @{term "st_set(A)"} makes the definition slightly
   51.17 +    \<comment>\<open>the condition @{term "st_set(A)"} makes the definition slightly
   51.18           stronger than the HOL one\<close>
   51.19  
   51.20  definition unless :: "[i, i] => i"  (infixl "unless" 60)  where
   51.21 @@ -199,7 +199,7 @@
   51.22       "Pow(state*state) \<subseteq> AllowedActs(F) \<longleftrightarrow> AllowedActs(F)=Pow(state*state)"
   51.23  by (cut_tac F = F in AllowedActs_type, auto)
   51.24  
   51.25 -subsubsection\<open>Eliminating @{text "\<inter> state"} from expressions\<close>
   51.26 +subsubsection\<open>Eliminating \<open>\<inter> state\<close> from expressions\<close>
   51.27  
   51.28  lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)"
   51.29  by (cut_tac F = F in Init_type, blast)
    52.1 --- a/src/ZF/UNITY/WFair.thy	Mon Dec 07 10:19:30 2015 +0100
    52.2 +++ b/src/ZF/UNITY/WFair.thy	Mon Dec 07 10:23:50 2015 +0100
    52.3 @@ -283,7 +283,7 @@
    52.4  lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto> B) \<longleftrightarrow>  (\<forall>A \<in> S. F \<in> A \<longmapsto> B) & F \<in> program & st_set(B)"
    52.5  by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)
    52.6  
    52.7 -text\<open>Set difference: maybe combine with @{text leadsTo_weaken_L}??\<close>
    52.8 +text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??\<close>
    52.9  lemma leadsTo_Diff:
   52.10       "[| F: (A-B) \<longmapsto> C; F \<in> B \<longmapsto> C; st_set(C) |]
   52.11        ==> F \<in> A \<longmapsto> C"
    53.1 --- a/src/ZF/Univ.thy	Mon Dec 07 10:19:30 2015 +0100
    53.2 +++ b/src/ZF/Univ.thy	Mon Dec 07 10:23:50 2015 +0100
    53.3 @@ -77,7 +77,7 @@
    53.4  apply (subst Vfrom)
    53.5  apply (subst Vfrom, rule subset_refl [THEN Un_mono])
    53.6  apply (rule UN_least)
    53.7 -txt\<open>expand @{text "rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))"} in assumptions\<close>
    53.8 +txt\<open>expand \<open>rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))\<close> in assumptions\<close>
    53.9  apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
   53.10  apply (rule subset_trans)
   53.11  apply (erule_tac [2] UN_upper)
   53.12 @@ -748,7 +748,7 @@
   53.13       "[| f: W -||> univ(A);  W \<subseteq> univ(A) |] ==> f \<in> univ(A)"
   53.14  by (erule FiniteFun_univ [THEN subsetD], assumption)
   53.15  
   53.16 -text\<open>Remove @{text "\<subseteq>"} from the rule above\<close>
   53.17 +text\<open>Remove \<open>\<subseteq>\<close> from the rule above\<close>
   53.18  lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
   53.19  
   53.20  
    54.1 --- a/src/ZF/WF.thy	Mon Dec 07 10:19:30 2015 +0100
    54.2 +++ b/src/ZF/WF.thy	Mon Dec 07 10:23:50 2015 +0100
    54.3 @@ -116,7 +116,7 @@
    54.4  
    54.5  lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]
    54.6  
    54.7 -text\<open>The form of this rule is designed to match @{text wfI}\<close>
    54.8 +text\<open>The form of this rule is designed to match \<open>wfI\<close>\<close>
    54.9  lemma wf_induct2:
   54.10      "[| wf(r);  a \<in> A;  field(r)<=A;
   54.11          !!x.[| x \<in> A;  \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
   54.12 @@ -287,7 +287,7 @@
   54.13  apply (rule_tac f = "\<lambda>y\<in>r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
   54.14    apply typecheck
   54.15  apply (unfold is_recfun_def wftrec_def)
   54.16 -  --\<open>Applying the substitution: must keep the quantified assumption!\<close>
   54.17 +  \<comment>\<open>Applying the substitution: must keep the quantified assumption!\<close>
   54.18  apply (rule lam_cong [OF refl])
   54.19  apply (drule underD)
   54.20  apply (fold is_recfun_def)
    55.1 --- a/src/ZF/ZF.thy	Mon Dec 07 10:19:30 2015 +0100
    55.2 +++ b/src/ZF/ZF.thy	Mon Dec 07 10:23:50 2015 +0100
    55.3 @@ -15,9 +15,9 @@
    55.4  instance i :: "term" ..
    55.5  
    55.6  axiomatization
    55.7 -  zero :: "i"  ("0")   --\<open>the empty set\<close>  and
    55.8 -  Pow :: "i => i"  --\<open>power sets\<close>  and
    55.9 -  Inf :: "i"  --\<open>infinite set\<close>
   55.10 +  zero :: "i"  ("0")   \<comment>\<open>the empty set\<close>  and
   55.11 +  Pow :: "i => i"  \<comment>\<open>power sets\<close>  and
   55.12 +  Inf :: "i"  \<comment>\<open>infinite set\<close>
   55.13  
   55.14  text \<open>Bounded Quantifiers\<close>
   55.15  consts
   55.16 @@ -56,7 +56,7 @@
   55.17    Pair  :: "[i, i] => i"
   55.18    fst   :: "i => i"
   55.19    snd   :: "i => i"
   55.20 -  split :: "[[i, i] => 'a, i] => 'a::{}"  --\<open>for pattern-matching\<close>
   55.21 +  split :: "[[i, i] => 'a, i] => 'a::{}"  \<comment>\<open>for pattern-matching\<close>
   55.22  
   55.23  text \<open>Sigma and Pi Operators\<close>
   55.24  consts
   55.25 @@ -69,35 +69,35 @@
   55.26    range       :: "i => i"
   55.27    field       :: "i => i"
   55.28    converse    :: "i => i"
   55.29 -  relation    :: "i => o"        --\<open>recognizes sets of pairs\<close>
   55.30 -  "function"  :: "i => o"        --\<open>recognizes functions; can have non-pairs\<close>
   55.31 +  relation    :: "i => o"        \<comment>\<open>recognizes sets of pairs\<close>
   55.32 +  "function"  :: "i => o"        \<comment>\<open>recognizes functions; can have non-pairs\<close>
   55.33    Lambda      :: "[i, i => i] => i"
   55.34    restrict    :: "[i, i] => i"
   55.35  
   55.36  text \<open>Infixes in order of decreasing precedence\<close>
   55.37  consts
   55.38  
   55.39 -  Image       :: "[i, i] => i"    (infixl "``" 90) --\<open>image\<close>
   55.40 -  vimage      :: "[i, i] => i"    (infixl "-``" 90) --\<open>inverse image\<close>
   55.41 -  "apply"     :: "[i, i] => i"    (infixl "`" 90) --\<open>function application\<close>
   55.42 -  "Int"       :: "[i, i] => i"    (infixl "Int" 70) --\<open>binary intersection\<close>
   55.43 -  "Un"        :: "[i, i] => i"    (infixl "Un" 65) --\<open>binary union\<close>
   55.44 -  Diff        :: "[i, i] => i"    (infixl "-" 65) --\<open>set difference\<close>
   55.45 -  Subset      :: "[i, i] => o"    (infixl "<=" 50) --\<open>subset relation\<close>
   55.46 +  Image       :: "[i, i] => i"    (infixl "``" 90) \<comment>\<open>image\<close>
   55.47 +  vimage      :: "[i, i] => i"    (infixl "-``" 90) \<comment>\<open>inverse image\<close>
   55.48 +  "apply"     :: "[i, i] => i"    (infixl "`" 90) \<comment>\<open>function application\<close>
   55.49 +  "Int"       :: "[i, i] => i"    (infixl "Int" 70) \<comment>\<open>binary intersection\<close>
   55.50 +  "Un"        :: "[i, i] => i"    (infixl "Un" 65) \<comment>\<open>binary union\<close>
   55.51 +  Diff        :: "[i, i] => i"    (infixl "-" 65) \<comment>\<open>set difference\<close>
   55.52 +  Subset      :: "[i, i] => o"    (infixl "<=" 50) \<comment>\<open>subset relation\<close>
   55.53  
   55.54  axiomatization
   55.55 -  mem         :: "[i, i] => o"    (infixl ":" 50) --\<open>membership relation\<close>
   55.56 +  mem         :: "[i, i] => o"    (infixl ":" 50) \<comment>\<open>membership relation\<close>
   55.57  
   55.58  abbreviation
   55.59 -  not_mem :: "[i, i] => o"  (infixl "~:" 50)  --\<open>negated membership relation\<close>
   55.60 +  not_mem :: "[i, i] => o"  (infixl "~:" 50)  \<comment>\<open>negated membership relation\<close>
   55.61    where "x ~: y == ~ (x : y)"
   55.62  
   55.63  abbreviation
   55.64 -  cart_prod :: "[i, i] => i"    (infixr "*" 80) --\<open>Cartesian product\<close>
   55.65 +  cart_prod :: "[i, i] => i"    (infixr "*" 80) \<comment>\<open>Cartesian product\<close>
   55.66    where "A * B == Sigma(A, %_. B)"
   55.67  
   55.68  abbreviation
   55.69 -  function_space :: "[i, i] => i"  (infixr "->" 60) --\<open>function space\<close>
   55.70 +  function_space :: "[i, i] => i"  (infixr "->" 60) \<comment>\<open>function space\<close>
   55.71    where "A -> B == Pi(A, %_. B)"
   55.72  
   55.73  
   55.74 @@ -616,8 +616,8 @@
   55.75  
   55.76  declare Pow_iff [iff]
   55.77  
   55.78 -lemmas Pow_bottom = empty_subsetI [THEN PowI]    --\<open>@{term"0 \<in> Pow(B)"}\<close>
   55.79 -lemmas Pow_top = subset_refl [THEN PowI]         --\<open>@{term"A \<in> Pow(A)"}\<close>
   55.80 +lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
   55.81 +lemmas Pow_top = subset_refl [THEN PowI]         \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
   55.82  
   55.83  
   55.84  subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
    56.1 --- a/src/ZF/Zorn.thy	Mon Dec 07 10:19:30 2015 +0100
    56.2 +++ b/src/ZF/Zorn.thy	Mon Dec 07 10:23:50 2015 +0100
    56.3 @@ -114,7 +114,7 @@
    56.4       ==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
    56.5  apply (erule TFin_induct)
    56.6  apply (rule impI [THEN ballI])
    56.7 -txt\<open>case split using @{text TFin_linear_lemma1}\<close>
    56.8 +txt\<open>case split using \<open>TFin_linear_lemma1\<close>\<close>
    56.9  apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
   56.10         assumption+)
   56.11  apply (blast del: subsetI
   56.12 @@ -176,7 +176,7 @@
   56.13  
   56.14  subsection\<open>Hausdorff's Theorem: Every Set Contains a Maximal Chain\<close>
   56.15  
   56.16 -text\<open>NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
   56.17 +text\<open>NOTE: We assume the partial ordering is \<open>\<subseteq>\<close>, the subset
   56.18  relation!\<close>
   56.19  
   56.20  text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>
   56.21 @@ -248,7 +248,7 @@
   56.22  apply (unfold chain_def)
   56.23  apply (rule CollectI, blast, safe)
   56.24  apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
   56.25 -      txt\<open>@{text "Blast_tac's"} slow\<close>
   56.26 +      txt\<open>\<open>Blast_tac's\<close> slow\<close>
   56.27  done
   56.28  
   56.29  theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)"
   56.30 @@ -404,7 +404,7 @@
   56.31  prefer 2 apply (blast elim: equalityE)
   56.32  apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
   56.33  prefer 2 apply (blast elim: equalityE)
   56.34 -txt\<open>For proving @{text "x \<in> next`\<Union>(...)"}.
   56.35 +txt\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>.
   56.36    Abrial and Laffitte's justification appears to be faulty.\<close>
   56.37  apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y}) 
   56.38                      \<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
   56.39 @@ -449,7 +449,7 @@
   56.40    shows "\<exists>m\<in>field(r). \<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
   56.41  proof -
   56.42    have "Preorder(r)" using po by (simp add: partial_order_on_def)
   56.43 -  --\<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close>
   56.44 +  \<comment>\<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close>
   56.45    let ?B = "\<lambda>x\<in>field(r). r -`` {x}" let ?S = "?B `` field(r)"
   56.46    have "\<forall>C\<in>chain(?S). \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
   56.47    proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
    57.1 --- a/src/ZF/equalities.thy	Mon Dec 07 10:19:30 2015 +0100
    57.2 +++ b/src/ZF/equalities.thy	Mon Dec 07 10:23:50 2015 +0100
    57.3 @@ -20,7 +20,7 @@
    57.4  text \<open>\medskip
    57.5  
    57.6    The following are not added to the default simpset because
    57.7 -  (a) they duplicate the body and (b) there are no similar rules for @{text Int}.\<close>
    57.8 +  (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
    57.9  
   57.10  lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"
   57.11    by blast
    58.1 --- a/src/ZF/ex/CoUnit.thy	Mon Dec 07 10:19:30 2015 +0100
    58.2 +++ b/src/ZF/ex/CoUnit.thy	Mon Dec 07 10:23:50 2015 +0100
    58.3 @@ -25,14 +25,14 @@
    58.4    "counit" = Con ("x \<in> counit")
    58.5  
    58.6  inductive_cases ConE: "Con(x) \<in> counit"
    58.7 -  -- \<open>USELESS because folding on @{term "Con(xa) == xa"} fails.\<close>
    58.8 +  \<comment> \<open>USELESS because folding on @{term "Con(xa) == xa"} fails.\<close>
    58.9  
   58.10  lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y"
   58.11 -  -- \<open>Proving freeness results.\<close>
   58.12 +  \<comment> \<open>Proving freeness results.\<close>
   58.13    by (auto elim!: counit.free_elims)
   58.14  
   58.15  lemma counit_eq_univ: "counit = quniv(0)"
   58.16 -  -- \<open>Should be a singleton, not everything!\<close>
   58.17 +  \<comment> \<open>Should be a singleton, not everything!\<close>
   58.18    apply (rule counit.dom_subset [THEN equalityI])
   58.19    apply (rule subsetI)
   58.20    apply (erule counit.coinduct)
   58.21 @@ -56,7 +56,7 @@
   58.22  inductive_cases Con2E: "Con2(x, y) \<in> counit2"
   58.23  
   58.24  lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'"
   58.25 -  -- \<open>Proving freeness results.\<close>
   58.26 +  \<comment> \<open>Proving freeness results.\<close>
   58.27    by (fast elim!: counit2.free_elims)
   58.28  
   58.29  lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))"
   58.30 @@ -74,7 +74,7 @@
   58.31  
   58.32  lemma counit2_Int_Vset_subset [rule_format]:
   58.33    "Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y"
   58.34 -  -- \<open>Lemma for proving finality.\<close>
   58.35 +  \<comment> \<open>Lemma for proving finality.\<close>
   58.36    apply (erule trans_induct)
   58.37    apply (tactic "safe_tac (put_claset subset_cs @{context})")
   58.38    apply (erule counit2.cases)
    59.1 --- a/src/ZF/ex/Group.thy	Mon Dec 07 10:19:30 2015 +0100
    59.2 +++ b/src/ZF/ex/Group.thy	Mon Dec 07 10:23:50 2015 +0100
    59.3 @@ -274,14 +274,14 @@
    59.4  
    59.5  text \<open>
    59.6    Since @{term H} is nonempty, it contains some element @{term x}.  Since
    59.7 -  it is closed under inverse, it contains @{text "inv x"}.  Since
    59.8 -  it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
    59.9 +  it is closed under inverse, it contains \<open>inv x\<close>.  Since
   59.10 +  it is closed under product, it contains \<open>x \<cdot> inv x = \<one>\<close>.
   59.11  \<close>
   59.12  
   59.13  text \<open>
   59.14    Since @{term H} is nonempty, it contains some element @{term x}.  Since
   59.15 -  it is closed under inverse, it contains @{text "inv x"}.  Since
   59.16 -  it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
   59.17 +  it is closed under inverse, it contains \<open>inv x\<close>.  Since
   59.18 +  it is closed under product, it contains \<open>x \<cdot> inv x = \<one>\<close>.
   59.19  \<close>
   59.20  
   59.21  lemma (in group) one_in_subset:
   59.22 @@ -628,7 +628,7 @@
   59.23  
   59.24  lemma (in group) coset_join2:
   59.25       "\<lbrakk>x \<in> carrier(G);  subgroup(H,G);  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
   59.26 -  --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
   59.27 +  \<comment>\<open>Alternative proof is to put @{term "x=\<one>"} in \<open>repr_independence\<close>.\<close>
   59.28  by (force simp add: subgroup.m_closed r_coset_def solve_equation)
   59.29  
   59.30  lemma (in group) r_coset_subset_G:
   59.31 @@ -788,7 +788,7 @@
   59.32  done
   59.33  
   59.34  
   59.35 -subsubsection \<open>Set of inverses of an @{text r_coset}.\<close>
   59.36 +subsubsection \<open>Set of inverses of an \<open>r_coset\<close>.\<close>
   59.37  
   59.38  lemma (in normal) rcos_inv:
   59.39    assumes x:     "x \<in> carrier(G)"
   59.40 @@ -817,7 +817,7 @@
   59.41  
   59.42  
   59.43  
   59.44 -subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
   59.45 +subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
   59.46  
   59.47  lemma (in group) setmult_rcos_assoc:
   59.48       "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
   59.49 @@ -852,7 +852,7 @@
   59.50  by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   59.51  
   59.52  lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   59.53 -  -- \<open>generalizes @{text subgroup_mult_id}\<close>
   59.54 +  \<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
   59.55    by (auto simp add: RCOSETS_def subset
   59.56          setmult_rcos_assoc subgroup_mult_id normal_axioms normal.axioms)
   59.57  
   59.58 @@ -897,7 +897,7 @@
   59.59    qed
   59.60  qed
   59.61  
   59.62 -text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
   59.63 +text\<open>Equivalence classes of \<open>rcong\<close> correspond to left cosets.
   59.64    Was there a mistake in the definitions? I'd have expected them to
   59.65    correspond to right cosets.\<close>
   59.66  lemma (in subgroup) l_coset_eq_rcong:
   59.67 @@ -1021,7 +1021,7 @@
   59.68  
   59.69  definition
   59.70    FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
   59.71 -    --\<open>Actually defined for groups rather than monoids\<close>
   59.72 +    \<comment>\<open>Actually defined for groups rather than monoids\<close>
   59.73    "G Mod H ==
   59.74       <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
   59.75  
   59.76 @@ -1085,7 +1085,7 @@
   59.77  
   59.78  definition
   59.79    kernel :: "[i,i,i] => i" where
   59.80 -    --\<open>the kernel of a homomorphism\<close>
   59.81 +    \<comment>\<open>the kernel of a homomorphism\<close>
   59.82    "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}"
   59.83  
   59.84  lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
   59.85 @@ -1215,7 +1215,7 @@
   59.86    hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}"
   59.87      by (auto simp add: y kernel_def r_coset_def)
   59.88    with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
   59.89 -        --\<open>The witness is @{term "kernel(G,H,h) #> g"}\<close>
   59.90 +        \<comment>\<open>The witness is @{term "kernel(G,H,h) #> g"}\<close>
   59.91      by (force simp add: FactGroup_def RCOSETS_def
   59.92             image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
   59.93  qed
    60.1 --- a/src/ZF/ex/Limit.thy	Mon Dec 07 10:19:30 2015 +0100
    60.2 +++ b/src/ZF/ex/Limit.thy	Mon Dec 07 10:23:50 2015 +0100
    60.3 @@ -1295,7 +1295,7 @@
    60.4  apply (simp add: Dinf_def [symmetric])
    60.5  apply (rule ballI)
    60.6  apply (simplesubst lub_iprod)
    60.7 -  --\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
    60.8 +  \<comment>\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
    60.9  apply (assumption | rule chain_Dinf emb_chain_cpo)+
   60.10  apply simp
   60.11  apply (subst Rp_cont [THEN cont_lub])
   60.12 @@ -1736,7 +1736,7 @@
   60.13     apply blast
   60.14    apply assumption
   60.15   apply (simplesubst eps_split_right_le)
   60.16 -    --\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
   60.17 +    \<comment>\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
   60.18         prefer 2 apply assumption
   60.19        apply simp
   60.20       apply (assumption | rule add_le_self nat_0I nat_succI)+
    61.1 --- a/src/ZF/ex/Primes.thy	Mon Dec 07 10:19:30 2015 +0100
    61.2 +++ b/src/ZF/ex/Primes.thy	Mon Dec 07 10:23:50 2015 +0100
    61.3 @@ -12,22 +12,22 @@
    61.4      "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
    61.5  
    61.6  definition
    61.7 -  is_gcd  :: "[i,i,i]=>o"     --\<open>definition of great common divisor\<close>  where
    61.8 +  is_gcd  :: "[i,i,i]=>o"     \<comment>\<open>definition of great common divisor\<close>  where
    61.9      "is_gcd(p,m,n) == ((p dvd m) & (p dvd n))   &
   61.10                         (\<forall>d\<in>nat. (d dvd m) & (d dvd n) \<longrightarrow> d dvd p)"
   61.11  
   61.12  definition
   61.13 -  gcd     :: "[i,i]=>i"       --\<open>Euclid's algorithm for the gcd\<close>  where
   61.14 +  gcd     :: "[i,i]=>i"       \<comment>\<open>Euclid's algorithm for the gcd\<close>  where
   61.15      "gcd(m,n) == transrec(natify(n),
   61.16                          %n f. \<lambda>m \<in> nat.
   61.17                                  if n=0 then m else f`(m mod n)`n) ` natify(m)"
   61.18  
   61.19  definition
   61.20 -  coprime :: "[i,i]=>o"       --\<open>the coprime relation\<close>  where
   61.21 +  coprime :: "[i,i]=>o"       \<comment>\<open>the coprime relation\<close>  where
   61.22      "coprime(m,n) == gcd(m,n) = 1"
   61.23    
   61.24  definition
   61.25 -  prime   :: i                --\<open>the set of prime numbers\<close>  where
   61.26 +  prime   :: i                \<comment>\<open>the set of prime numbers\<close>  where
   61.27     "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p \<longrightarrow> m=1 | m=p)}"
   61.28  
   61.29  
    62.1 --- a/src/ZF/ex/Ramsey.thy	Mon Dec 07 10:19:30 2015 +0100
    62.2 +++ b/src/ZF/ex/Ramsey.thy	Mon Dec 07 10:23:50 2015 +0100
    62.3 @@ -31,7 +31,7 @@
    62.4      "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)"
    62.5  
    62.6  definition
    62.7 -  Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality"
    62.8 +  Atleast :: "[i,i]=>o" where \<comment> "not really necessary: ZF defines cardinality"
    62.9      "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))"
   62.10  
   62.11  definition
    63.1 --- a/src/ZF/ex/misc.thy	Mon Dec 07 10:19:30 2015 +0100
    63.2 +++ b/src/ZF/ex/misc.thy	Mon Dec 07 10:23:50 2015 +0100
    63.3 @@ -19,11 +19,11 @@
    63.4  
    63.5  lemma singleton_example_2:
    63.6       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    63.7 -  -- \<open>Variant of the problem above.\<close>
    63.8 +  \<comment> \<open>Variant of the problem above.\<close>
    63.9    by blast
   63.10  
   63.11  lemma "\<exists>!x. f (g(x)) = x \<Longrightarrow> \<exists>!y. g (f(y)) = y"
   63.12 -  -- \<open>A unique fixpoint theorem --- @{text fast}/@{text best}/@{text auto} all fail.\<close> 
   63.13 +  \<comment> \<open>A unique fixpoint theorem --- \<open>fast\<close>/\<open>best\<close>/\<open>auto\<close> all fail.\<close> 
   63.14    apply (erule ex1E, rule ex1I, erule subst_context)
   63.15    apply (rule subst, assumption, erule allE, rule subst_context, erule mp)
   63.16    apply (erule subst_context)
    64.1 --- a/src/ZF/upair.thy	Mon Dec 07 10:19:30 2015 +0100
    64.2 +++ b/src/ZF/upair.thy	Mon Dec 07 10:23:50 2015 +0100
    64.3 @@ -195,7 +195,7 @@
    64.4  by blast
    64.5  
    64.6  
    64.7 -subsection\<open>Conditional Terms: @{text "if-then-else"}\<close>
    64.8 +subsection\<open>Conditional Terms: \<open>if-then-else\<close>\<close>
    64.9  
   64.10  lemma if_true [simp]: "(if True then a else b) = a"
   64.11  by (unfold if_def, blast)