--- a/src/HOL/simpdata.ML Wed Dec 06 01:12:51 2006 +0100
+++ b/src/HOL/simpdata.ML Wed Dec 06 01:12:56 2006 +0100
@@ -163,19 +163,29 @@
structure Splitter = SplitterFun(SplitterData);
+val split_tac = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+
+val op addsplits = Splitter.addsplits;
+val op delsplits = Splitter.delsplits;
+val Addsplits = Splitter.Addsplits;
+val Delsplits = Splitter.Delsplits;
+
+
(* integration of simplifier with classical reasoner *)
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
and Classical = Classical and Blast = Blast
- val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
+ val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE")
+open Clasimp;
val mksimps_pairs =
[("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
("All", [thm "spec"]), ("True", []), ("False", []),
("HOL.If", [thm "if_bool_eq_conj" RS thm "iffD1"])];
-val simpset_basic =
+val HOL_basic_ss =
Simplifier.theory_context (the_context ()) empty_ss
setsubgoaler asm_simp_tac
setSSolver safe_solver
@@ -184,10 +194,10 @@
setmkeqTrue mk_eq_True
setmkcong mk_meta_cong;
-fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
+fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
fun unfold_tac ths =
- let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
+ let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
@@ -338,7 +348,7 @@
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
-val simpset_simprocs = simpset_basic
+val simpset_simprocs = HOL_basic_ss
addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
end;