--- a/src/HOL/Set.ML Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/Set.ML Sun Oct 14 20:02:59 2001 +0200
@@ -844,12 +844,12 @@
(* rulify setup *)
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 = HOL_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
--- a/src/HOL/arith_data.ML Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/arith_data.ML Sun Oct 14 20:02:59 2001 +0200
@@ -422,7 +422,7 @@
in
-val arith_tac = fast_arith_tac ORELSE' (atomize_tac THEN' raw_arith_tac);
+val arith_tac = fast_arith_tac ORELSE' (ObjectLogic.atomize_tac THEN' raw_arith_tac);
fun arith_method prems =
Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
--- a/src/HOL/blastdata.ML Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/blastdata.ML Sun Oct 14 20:02:59 2001 +0200
@@ -23,7 +23,6 @@
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset = Classical.claset
val rep_cs = Classical.rep_cs
- val atomize = atomize_rules
val cla_modifiers = Classical.cla_modifiers;
val cla_meth' = Classical.cla_meth'
end;
--- a/src/HOL/cladata.ML Sun Oct 14 20:02:30 2001 +0200
+++ b/src/HOL/cladata.ML Sun Oct 14 20:02:59 2001 +0200
@@ -38,10 +38,6 @@
compatibliity with strange things done in many existing proofs *)
val cla_make_elim = Make_Elim.make_elim;
-val atomize_rules = thms "atomize'";
-val atomize_tac = Method.atomize_tac atomize_rules;
-val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
-
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
@@ -51,7 +47,6 @@
val classical = classical
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
- val atomize = atomize_rules
end;
structure Classical = ClassicalFun(Classical_Data);