--- a/src/ZF/Constructible/Formula.thy Mon Nov 18 14:51:44 2002 +0100
+++ b/src/ZF/Constructible/Formula.thy Tue Nov 19 10:41:20 2002 +0100
@@ -475,7 +475,7 @@
text{*@{term DPow} is not monotonic. For example, let @{term A} be some
non-constructible set of natural numbers, and let @{term B} be @{term nat}.
-Then @{term "A<=B"} and obviously @{term "A : DPow(A)"} but @{term "A ~:
+Then @{term "A<=B"} and obviously @{term "A \<in> DPow(A)"} but @{term "A ~:
DPow(B)"}.*}
(*This may be true but the proof looks difficult, requiring relativization
@@ -694,7 +694,7 @@
"Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
by (simp add: Lset_Union [symmetric] Limit_Union_eq)
-lemma lt_LsetI: "[| a: Lset(j); j<i |] ==> a : Lset(i)"
+lemma lt_LsetI: "[| a: Lset(j); j<i |] ==> a \<in> Lset(i)"
by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
lemma Limit_LsetE:
@@ -710,7 +710,7 @@
subsubsection{* Basic closure properties *}
-lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
+lemma zero_in_Lset: "y:x ==> 0 \<in> Lset(x)"
by (subst Lset, blast intro: empty_in_DPow)
lemma notin_Lset: "x \<notin> Lset(x)"
@@ -774,15 +774,15 @@
subsubsection{* Finite sets and ordered pairs *}
-lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
+lemma singleton_in_Lset: "a: Lset(i) ==> {a} \<in> Lset(succ(i))"
by (simp add: Lset_succ singleton_in_DPow)
lemma doubleton_in_Lset:
- "[| a: Lset(i); b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
+ "[| a: Lset(i); b: Lset(i) |] ==> {a,b} \<in> Lset(succ(i))"
by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
lemma Pair_in_Lset:
- "[| a: Lset(i); b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
+ "[| a: Lset(i); b: Lset(i); Ord(i) |] ==> <a,b> \<in> Lset(succ(succ(i)))"
apply (unfold Pair_def)
apply (blast intro: doubleton_in_Lset)
done
@@ -792,7 +792,7 @@
text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
lemma doubleton_in_LLimit:
- "[| a: Lset(i); b: Lset(i); Limit(i) |] ==> {a,b} : Lset(i)"
+ "[| a: Lset(i); b: Lset(i); Limit(i) |] ==> {a,b} \<in> Lset(i)"
apply (erule Limit_LsetE, assumption)
apply (erule Limit_LsetE, assumption)
apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
@@ -806,7 +806,7 @@
done
lemma Pair_in_LLimit:
- "[| a: Lset(i); b: Lset(i); Limit(i) |] ==> <a,b> : Lset(i)"
+ "[| a: Lset(i); b: Lset(i); Limit(i) |] ==> <a,b> \<in> Lset(i)"
txt{*Infer that a, b occur at ordinals x,xa < i.*}
apply (erule Limit_LsetE, assumption)
apply (erule Limit_LsetE, assumption)
@@ -919,7 +919,7 @@
subsubsection{*For L to satisfy the Powerset axiom *}
lemma LPow_env_typing:
- "[| y : Lset(i); Ord(i); y \<subseteq> X |]
+ "[| y \<in> Lset(i); Ord(i); y \<subseteq> X |]
==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
by (auto intro: L_I iff: Lset_succ_lrank_iff)
--- a/src/ZF/Constructible/Rank.thy Mon Nov 18 14:51:44 2002 +0100
+++ b/src/ZF/Constructible/Rank.thy Tue Nov 19 10:41:20 2002 +0100
@@ -129,7 +129,7 @@
lemma ord_iso_converse1:
"[| f: ord_iso(A,r,B,s); <b, f`a>: s; a:A; b:B |]
- ==> <converse(f) ` b, a> : r"
+ ==> <converse(f) ` b, a> \<in> r"
apply (frule ord_iso_converse, assumption+)
apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype])
apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
@@ -290,9 +290,9 @@
apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f i]])
apply (rename_tac c j, clarify)
apply (frule omap_funtype [of A r f, THEN apply_funtype], assumption+)
-apply (subgoal_tac "j : i")
+apply (subgoal_tac "j \<in> i")
prefer 2 apply (blast intro: Ord_trans Ord_otype)
-apply (subgoal_tac "converse(f) ` j : obase(M,A,r)")
+apply (subgoal_tac "converse(f) ` j \<in> obase(M,A,r)")
prefer 2
apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij,
THEN bij_is_fun, THEN apply_funtype])
--- a/src/ZF/Constructible/WFrec.thy Mon Nov 18 14:51:44 2002 +0100
+++ b/src/ZF/Constructible/WFrec.thy Tue Nov 19 10:41:20 2002 +0100
@@ -105,7 +105,7 @@
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
apply (rename_tac x1)
apply (rule_tac t="%z. H(x1,z)" in subst_context)
-apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g")
+apply (subgoal_tac "\<forall>y \<in> r-``{x1}. ALL z. <y,z>\<in>f <-> <y,z>\<in>g")
apply (blast intro: transD)
apply (simp add: apply_iff)
apply (blast intro: transD sym)
--- a/src/ZF/Constructible/document/root.tex Mon Nov 18 14:51:44 2002 +0100
+++ b/src/ZF/Constructible/document/root.tex Tue Nov 19 10:41:20 2002 +0100
@@ -5,8 +5,8 @@
%table of contents too crowded!
\usepackage{tocloft}
-\addtolength{\cftsubsecnumwidth}{0.5em}
-\addtolength{\cftsubsubsecnumwidth}{1.0em}
+\addtolength\cftsubsecnumwidth {0.5em}
+\addtolength\cftsubsubsecnumwidth {1.0em}
\begin{document}