# HG changeset patch
# User nipkow
# Date 833364212 -7200
# Node ID 608050b43bee4914cf12b9a024a22549b7c51786
# Parent  abdab44dcb8b3289a8402429e908d504ce9c9fe5
Added addsolver

diff -r abdab44dcb8b -r 608050b43bee src/Provers/simplifier.ML
--- 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,