--- a/src/Provers/simplifier.ML Tue May 28 11:19:16 1996 +0200
+++ b/src/Provers/simplifier.ML Wed May 29 12:03:32 1996 +0200
@@ -7,7 +7,7 @@
*)
-infix 4 addsimps addeqcongs delsimps
+infix 4 addsimps addeqcongs addsolver delsimps
setsolver setloop setmksimps setsubgoaler;
signature SIMPLIFIER =
@@ -15,6 +15,7 @@
type simpset
val addeqcongs: simpset * thm list -> simpset
val addsimps: simpset * thm list -> simpset
+ val addsolver: simpset * (thm list -> int -> tactic) -> simpset
val delsimps: simpset * thm list -> simpset
val asm_full_simp_tac: simpset -> int -> tactic
val full_simp_tac: simpset -> int -> tactic
@@ -75,6 +76,14 @@
finish_tac=finish_tac,
loop_tac=loop_tac};
+fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,finish_tac}) addsolver tac =
+ Simpset{mss=mss,
+ simps= simps,
+ congs= congs,
+ subgoal_tac= subgoal_tac,
+ finish_tac=fn hyps => finish_tac hyps ORELSE' tac hyps,
+ loop_tac=loop_tac};
+
fun (Simpset{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler
subgoal_tac =
Simpset{mss=mss,