Mod because of new solver interface.
--- a/src/FOL/simpdata.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/FOL/simpdata.ML Tue Sep 21 19:11:07 1999 +0200
@@ -325,8 +325,8 @@
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
addsimprocs [defALL_regroup,defEX_regroup]
- setSSolver safe_solver
- setSolver unsafe_solver
+ setSSolver (mk_solver "FOL safe" safe_solver)
+ setSolver (mk_solver "FOL unsafe" unsafe_solver)
setmksimps (mksimps mksimps_pairs);
--- a/src/HOL/Arith.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/Arith.ML Tue Sep 21 19:11:07 1999 +0200
@@ -1000,7 +1000,8 @@
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
solver all the time rather than add the additional check. *)
-simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
+simpset_ref () := (simpset() addSolver
+ (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
(* Elimination of `-' on nat due to John Harrison *)
Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
--- a/src/HOL/List.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/List.ML Tue Sep 21 19:11:07 1999 +0200
@@ -804,6 +804,7 @@
by (exhaust_tac "na" 1);
by Auto_tac;
qed_spec_mp "take_take";
+Addsimps [take_take];
Goal "!xs. drop n (drop m xs) = drop (n + m) xs";
by (induct_tac "m" 1);
@@ -811,6 +812,7 @@
by (exhaust_tac "xs" 1);
by Auto_tac;
qed_spec_mp "drop_drop";
+Addsimps [drop_drop];
Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
by (induct_tac "m" 1);
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML Tue Sep 21 19:11:07 1999 +0200
@@ -28,7 +28,7 @@
let
val (cs,ss) = MI_css
in
- (cs addSEs [squareE], ss addSSolver (fn thms => assume_tac ORELSE' (etac notE)))
+ (cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
end;
val temp_elim = make_elim o temp_use;
--- a/src/HOL/WF.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/WF.ML Tue Sep 21 19:11:07 1999 +0200
@@ -260,7 +260,7 @@
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss addSolver indhyp_tac;
+val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
Goalw [is_recfun_def,cut_def]
"[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \
--- a/src/HOL/simpdata.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/simpdata.ML Tue Sep 21 19:11:07 1999 +0200
@@ -429,14 +429,18 @@
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
-fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems),
- atac , etac FalseE ];
+fun unsafe_solver_tac prems =
+ FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
+val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
+
(*No premature instantiation of variables during simplification*)
-fun safe_solver prems = FIRST'[ match_tac(reflexive_thm::TrueI::refl::prems),
- eq_assume_tac, ematch_tac [FalseE]];
+fun safe_solver_tac prems =
+ FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
+ eq_assume_tac, ematch_tac [FalseE]];
+val safe_solver = mk_solver "HOL safe" safe_solver_tac;
val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
- setSSolver safe_solver
+ setSSolver safe_solver
setSolver unsafe_solver
setmksimps (mksimps mksimps_pairs)
setmkeqTrue mk_eq_True;
--- a/src/HOLCF/HOLCF.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOLCF/HOLCF.ML Tue Sep 21 19:11:07 1999 +0200
@@ -8,7 +8,7 @@
use"adm.ML";
-simpset_ref() := simpset() addSolver(fn thms =>
- (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
+simpset_ref() := simpset() addSolver
+ (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
val HOLCF_ss = simpset();
--- a/src/HOLCF/Lift.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOLCF/Lift.ML Tue Sep 21 19:11:07 1999 +0200
@@ -71,7 +71,8 @@
REPEAT (cont_tac i);
-simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+simpset_ref() := simpset() addSolver
+ (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 21 19:11:07 1999 +0200
@@ -277,7 +277,7 @@
| mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD))
| mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
| mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD))
- | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp(prth(addthms (mk j1) (mk j2)))))
+ | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp((*prth*)(addthms (mk j1) (mk j2)))))
| mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j))
in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end
--- a/src/Sequents/simpdata.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/Sequents/simpdata.ML Tue Sep 21 19:11:07 1999 +0200
@@ -241,8 +241,8 @@
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
- setSSolver safe_solver
- setSolver unsafe_solver
+ setSSolver (mk_solver "safe" safe_solver)
+ setSolver (mk_solver "unsafe" unsafe_solver)
setmksimps (map mk_meta_eq o atomize o gen_all);
val LK_simps =
--- a/src/ZF/Order.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/Order.ML Tue Sep 21 19:11:07 1999 +0200
@@ -242,9 +242,9 @@
(*Rewriting with bijections and converse (function inverse)*)
val bij_inverse_ss =
- simpset() setSolver
- type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj,
- inj_is_fun, comp_fun, comp_bij])
+ simpset() setSolver (mk_solver ""
+ (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj,
+ inj_is_fun, comp_fun, comp_bij])))
addsimps [right_inverse_bij];
Goalw [ord_iso_def]
--- a/src/ZF/Perm.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/Perm.ML Tue Sep 21 19:11:07 1999 +0200
@@ -344,8 +344,8 @@
by (rtac lam_funtype 2);
by (typecheck_tac (tcset() addTCs [prem]));
by (asm_simp_tac (simpset()
- setSolver
- type_solver_tac (tcset() addTCs [prem, lam_funtype])) 1);
+ setSolver (mk_solver ""
+ (type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
qed "comp_lam";
Goal "[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)";
@@ -353,8 +353,8 @@
f_imp_injective 1);
by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
by (asm_simp_tac (simpset()
- setSolver
- type_solver_tac (tcset() addTCs [inj_is_fun])) 1);
+ setSolver (mk_solver ""
+ (type_solver_tac (tcset() addTCs [inj_is_fun])))) 1);
qed "comp_inj";
Goalw [surj_def]
--- a/src/ZF/Tools/inductive_package.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Sep 21 19:11:07 1999 +0200
@@ -335,9 +335,10 @@
If the premises get simplified, then the proofs could fail.*)
val min_ss = empty_ss
setmksimps (map mk_eq o ZF_atomize o gen_all)
- setSolver (fn prems => resolve_tac (triv_rls@prems)
+ setSolver (mk_solver "minimal"
+ (fn prems => resolve_tac (triv_rls@prems)
ORELSE' assume_tac
- ORELSE' etac FalseE);
+ ORELSE' etac FalseE));
val quant_induct =
prove_goalw_cterm part_rec_defs
--- a/src/ZF/WF.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/WF.ML Tue Sep 21 19:11:07 1999 +0200
@@ -229,7 +229,7 @@
eresolve_tac [underD, transD, spec RS mp]));
(*** NOTE! some simplifications need a different solver!! ***)
-val wf_super_ss = simpset() setSolver indhyp_tac;
+val wf_super_ss = simpset() setSolver (mk_solver "WF" indhyp_tac);
Goalw [is_recfun_def]
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
--- a/src/ZF/simpdata.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/simpdata.ML Tue Sep 21 19:11:07 1999 +0200
@@ -107,6 +107,6 @@
simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
addsplits [split_if]
- setSolver Type_solver_tac;
+ setSolver (mk_solver "types" Type_solver_tac);
val ZF_ss = simpset();