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