src/ZF/Constructible/Formula.thy
 changeset 13721 2cf506c09946 parent 13687 22dce9134953 child 14171 0cab06e3bbd0
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Mon Nov 18 14:51:44 2002 +0100
1.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Nov 19 10:41:20 2002 +0100
1.3 @@ -475,7 +475,7 @@
1.4
1.5  text{*@{term DPow} is not monotonic.  For example, let @{term A} be some
1.6  non-constructible set of natural numbers, and let @{term B} be @{term nat}.
1.7 -Then @{term "A<=B"} and obviously @{term "A : DPow(A)"} but @{term "A ~:
1.8 +Then @{term "A<=B"} and obviously @{term "A \<in> DPow(A)"} but @{term "A ~:
1.9  DPow(B)"}.*}
1.10
1.11  (*This may be true but the proof looks difficult, requiring relativization
1.12 @@ -694,7 +694,7 @@
1.13      "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
1.14  by (simp add: Lset_Union [symmetric] Limit_Union_eq)
1.15
1.16 -lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a : Lset(i)"
1.17 +lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a \<in> Lset(i)"
1.18  by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
1.19
1.20  lemma Limit_LsetE:
1.21 @@ -710,7 +710,7 @@
1.22
1.23  subsubsection{* Basic closure properties *}
1.24
1.25 -lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
1.26 +lemma zero_in_Lset: "y:x ==> 0 \<in> Lset(x)"
1.27  by (subst Lset, blast intro: empty_in_DPow)
1.28
1.29  lemma notin_Lset: "x \<notin> Lset(x)"
1.30 @@ -774,15 +774,15 @@
1.31
1.32  subsubsection{* Finite sets and ordered pairs *}
1.33
1.34 -lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
1.35 +lemma singleton_in_Lset: "a: Lset(i) ==> {a} \<in> Lset(succ(i))"
1.36  by (simp add: Lset_succ singleton_in_DPow)
1.37
1.38  lemma doubleton_in_Lset:
1.39 -     "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
1.40 +     "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} \<in> Lset(succ(i))"
1.41  by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
1.42
1.43  lemma Pair_in_Lset:
1.44 -    "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
1.45 +    "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> \<in> Lset(succ(succ(i)))"
1.46  apply (unfold Pair_def)
1.47  apply (blast intro: doubleton_in_Lset)
1.48  done
1.49 @@ -792,7 +792,7 @@
1.50
1.51  text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
1.52  lemma doubleton_in_LLimit:
1.53 -    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} : Lset(i)"
1.54 +    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} \<in> Lset(i)"
1.55  apply (erule Limit_LsetE, assumption)
1.56  apply (erule Limit_LsetE, assumption)
1.57  apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
1.58 @@ -806,7 +806,7 @@
1.59  done
1.60
1.61  lemma Pair_in_LLimit:
1.62 -    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> : Lset(i)"
1.63 +    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> \<in> Lset(i)"
1.64  txt{*Infer that a, b occur at ordinals x,xa < i.*}
1.65  apply (erule Limit_LsetE, assumption)
1.66  apply (erule Limit_LsetE, assumption)
1.67 @@ -919,7 +919,7 @@
1.68  subsubsection{*For L to satisfy the Powerset axiom *}
1.69
1.70  lemma LPow_env_typing:
1.71 -    "[| y : Lset(i); Ord(i); y \<subseteq> X |]
1.72 +    "[| y \<in> Lset(i); Ord(i); y \<subseteq> X |]
1.73       ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
1.74  by (auto intro: L_I iff: Lset_succ_lrank_iff)
1.75
```