--- a/src/ZF/ZF.ML Sun Oct 14 20:09:59 2001 +0200
+++ b/src/ZF/ZF.ML Sun Oct 14 20:10:44 2001 +0200
@@ -514,12 +514,12 @@
(* update rulify setup -- include bounded All *)
Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
-by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
-qed "ball_eq";
+by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
+qed "atomize_ball";
local
val ss = FOL_basic_ss addsimps
- (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
+ [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
in
structure Rulify = RulifyFun