src/ZF/Constructible/Relative.thy
changeset 13348 374d05460db4
parent 13339 0f89104dd377
child 13350 626b79677dfa
     1.1 --- a/src/ZF/Constructible/Relative.thy	Thu Jul 11 10:48:30 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Thu Jul 11 13:43:24 2002 +0200
     1.3 @@ -532,7 +532,7 @@
     1.4  done
     1.5  
     1.6  text{*Probably the premise and conclusion are equivalent*}
     1.7 -lemma (in M_triv_axioms) strong_replacementI [OF rallI]:
     1.8 +lemma (in M_triv_axioms) strong_replacementI [rule_format]:
     1.9      "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
    1.10       ==> strong_replacement(M,P)"
    1.11  apply (simp add: strong_replacement_def, clarify)