src/ZF/Constructible/Rank.thy
 changeset 61798 27f3c10b0b50 parent 60770 240563fbf41d child 67399 eab6ce8368fa
```     1.1 --- a/src/ZF/Constructible/Rank.thy	Mon Dec 07 10:19:30 2015 +0100
1.2 +++ b/src/ZF/Constructible/Rank.thy	Mon Dec 07 10:23:50 2015 +0100
1.3 @@ -15,7 +15,7 @@
1.4        ==> separation (M, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[M]. (\<exists>p[M].
1.5                       fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
1.6    and obase_separation:
1.7 -     --\<open>part of the order type formalization\<close>
1.8 +     \<comment>\<open>part of the order type formalization\<close>
1.9       "[| M(A); M(r) |]
1.10        ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
1.11               ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
1.12 @@ -92,7 +92,7 @@
1.13  text\<open>Following Kunen's Theorem I 7.6, page 17.  Note that this material is
1.14  not required elsewhere.\<close>
1.15
1.16 -text\<open>Can't use @{text well_ord_iso_preserving} because it needs the
1.17 +text\<open>Can't use \<open>well_ord_iso_preserving\<close> because it needs the
1.18  strong premise @{term "well_ord(A,r)"}\<close>
1.19  lemma (in M_ordertype) ord_iso_pred_imp_lt:
1.20       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
1.21 @@ -114,7 +114,7 @@
1.22  apply (frule restrict_ord_iso2, assumption+)
1.23  apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun])
1.24  apply (frule apply_type, blast intro: ltD)
1.25 -  --\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
1.26 +  \<comment>\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
1.28  apply (subgoal_tac
1.29         "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r,
1.30 @@ -137,26 +137,26 @@
1.31
1.32  definition
1.33    obase :: "[i=>o,i,i] => i" where
1.34 -       --\<open>the domain of @{text om}, eventually shown to equal @{text A}\<close>
1.35 +       \<comment>\<open>the domain of \<open>om\<close>, eventually shown to equal \<open>A\<close>\<close>
1.36     "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) &
1.37                            g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
1.38
1.39  definition
1.40    omap :: "[i=>o,i,i,i] => o" where
1.41 -    --\<open>the function that maps wosets to order types\<close>
1.42 +    \<comment>\<open>the function that maps wosets to order types\<close>
1.43     "omap(M,A,r,f) ==
1.44          \<forall>z[M].
1.45           z \<in> f \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) &
1.46                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
1.47
1.48  definition
1.49 -  otype :: "[i=>o,i,i,i] => o" where --\<open>the order types themselves\<close>
1.50 +  otype :: "[i=>o,i,i,i] => o" where \<comment>\<open>the order types themselves\<close>
1.51     "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
1.52
1.53
1.54  text\<open>Can also be proved with the premise @{term "M(z)"} instead of
1.55        @{term "M(f)"}, but that version is less useful.  This lemma
1.56 -      is also more useful than the definition, @{text omap_def}.\<close>
1.57 +      is also more useful than the definition, \<open>omap_def\<close>.\<close>
1.58  lemma (in M_ordertype) omap_iff:
1.59       "[| omap(M,A,r,f); M(A); M(f) |]
1.60        ==> z \<in> f \<longleftrightarrow>
1.61 @@ -478,7 +478,7 @@
1.62
1.63
1.64
1.65 -text\<open>@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF\<close>
1.66 +text\<open>\<open>is_oadd_fun\<close>: Relating the pure "language of set theory" to Isabelle/ZF\<close>
1.68     "[| a\<le>j; M(i); M(j); M(a); M(f) |]
1.70 @@ -602,7 +602,7 @@
1.71      "[| M(i); M(x); M(g); function(g) |]
1.72       ==> M(THE z. omult_eqns(i, x, g, z))"
1.73  apply (case_tac "Ord(x)")
1.74 - prefer 2 apply (simp add: omult_eqns_Not) --\<open>trivial, non-Ord case\<close>
1.75 + prefer 2 apply (simp add: omult_eqns_Not) \<comment>\<open>trivial, non-Ord case\<close>
1.76  apply (erule Ord_cases)
1.79 @@ -897,12 +897,12 @@
1.80  apply (frule is_recfun_restrict [of concl: "r^+" a])
1.81      apply (rule trans_trancl, assumption)
1.82     apply (simp_all add: r_into_trancl trancl_subset_times)
1.83 -txt\<open>Still the same goal, but with new @{text is_recfun} assumptions.\<close>
1.84 +txt\<open>Still the same goal, but with new \<open>is_recfun\<close> assumptions.\<close>