src/ZF/Constructible/Relative.thy

--- a/src/ZF/Constructible/Relative.thy	Thu Jul 11 10:48:30 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Thu Jul 11 13:43:24 2002 +0200
@@ -532,7 +532,7 @@
 done
 
 text{*Probably the premise and conclusion are equivalent*}
-lemma (in M_triv_axioms) strong_replacementI [OF rallI]:
+lemma (in M_triv_axioms) strong_replacementI [rule_format]:
     "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
      ==> strong_replacement(M,P)"
 apply (simp add: strong_replacement_def, clarify)