src/ZF/Constructible/Reflection.thy
changeset 58860 fee7cfa69c50
parent 46823 57bf0cecb366
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Constructible/Reflection.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/Constructible/Reflection.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -6,10 +6,10 @@
     1.4  
     1.5  theory Reflection imports Normal begin
     1.6  
     1.7 -lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))";
     1.8 +lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))"
     1.9  by blast
    1.10  
    1.11 -lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))";
    1.12 +lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))"
    1.13  by blast
    1.14  
    1.15  text{*From the notes of A. S. Kechris, page 6, and from
    1.16 @@ -339,14 +339,14 @@
    1.17  schematic_lemma (in reflection)
    1.18       "Reflects(?Cl,
    1.19                 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
    1.20 -               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
    1.21 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"
    1.22  by fast
    1.23  
    1.24  text{*Example 3''*}
    1.25  schematic_lemma (in reflection)
    1.26       "Reflects(?Cl,
    1.27                 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
    1.28 -               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
    1.29 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
    1.30  by fast
    1.31  
    1.32  text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs