1.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Sep 11 16:53:59 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Sep 11 16:55:37 2002 +0200
     1.3 @@ -127,7 +127,8 @@
     1.4    and successor_abs = M_trivial.successor_abs [OF M_trivial_L]
     1.5    and succ_in_M_iff = M_trivial.succ_in_M_iff [OF M_trivial_L]
     1.6    and separation_closed = M_trivial.separation_closed [OF M_trivial_L]
     1.7 -  and strong_replacementI = M_trivial.strong_replacementI [OF M_trivial_L]
     1.8 +  and strong_replacementI = 
     1.9 +      M_trivial.strong_replacementI [OF M_trivial_L, rule_format]
    1.10    and strong_replacement_closed = M_trivial.strong_replacement_closed [OF M_trivial_L]
    1.11    and RepFun_closed = M_trivial.RepFun_closed [OF M_trivial_L]
    1.12    and lam_closed = M_trivial.lam_closed [OF M_trivial_L]
    1.13 @@ -169,7 +170,6 @@
    1.14  declare successor_abs [simp]
    1.15  declare succ_in_M_iff [iff]
    1.16  declare separation_closed [intro, simp]
    1.17 -declare strong_replacementI
    1.18  declare strong_replacement_closed [intro, simp]
    1.19  declare RepFun_closed [intro, simp]
    1.20  declare lam_closed [intro, simp]