# HG changeset patch
# User paulson
# Date 1037698880 -3600
# Node ID 2cf506c09946eaa8b88313f65380a0ceb807a905
# Parent  be087f48b99f794cede42ed753aac55e93466185
stylistic tweaks

diff -r be087f48b99f -r 2cf506c09946 src/ZF/Constructible/Formula.thy
--- 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) 
 
diff -r be087f48b99f -r 2cf506c09946 src/ZF/Constructible/Rank.thy
--- 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])
diff -r be087f48b99f -r 2cf506c09946 src/ZF/Constructible/WFrec.thy
--- 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) 
diff -r be087f48b99f -r 2cf506c09946 src/ZF/Constructible/document/root.tex
--- 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}