src/ZF/Constructible/Reflection.thy

--- a/src/ZF/Constructible/Reflection.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/ZF/Constructible/Reflection.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -268,7 +268,7 @@
 text{*Example 1: reflecting a simple formula.  The reflecting class is first
 given as the variable @{text ?Cl} and later retrieved from the final 
 proof state.*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>x. \<exists>y. M(y) & x \<in> y, 
                \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
@@ -285,7 +285,7 @@
 
 
 text{*Example 2*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
                \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
@@ -302,14 +302,14 @@
 by fast
 
 text{*Example 2''.  We expand the subset relation.*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
   "Reflects(?Cl,
         \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
         \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
 by fast
 
 text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
                \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
@@ -329,21 +329,21 @@
 
 text{*Example 3.  Warning: the following examples make sense only
 if @{term P} is quantifier-free, since it is not being relativized.*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<in> y <-> z \<in> x & P(z)), 
                \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x & P(z))"
 by fast
 
 text{*Example 3'*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
                \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
 by fast
 
 text{*Example 3''*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
                \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
@@ -351,7 +351,7 @@
 
 text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
 to be relativized.*}
-lemma (in reflection) 
+schematic_lemma (in reflection) 
      "Reflects(?Cl,
                \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
                \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"