--- a/src/Provers/clasimp.ML Sat May 02 13:27:42 1998 +0200
+++ b/src/Provers/clasimp.ML Sat May 02 16:46:17 1998 +0200
@@ -24,6 +24,8 @@
val delsimps2 : clasimpset * thm list -> clasimpset
val addSss : claset * simpset -> claset
val addss : claset * simpset -> claset
+ val CLASIMPSET: (clasimpset -> tactic) -> tactic
+ val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic
val mk_auto_tac:clasimpset -> int -> int -> tactic
val auto_tac : clasimpset -> tactic
val Auto_tac : tactic
@@ -63,6 +65,10 @@
asm_full_simp_tac ss);
+fun CLASIMPSET tacf state = CLASET (fn cs => SIMPSET (fn ss => tacf (cs, ss))) state;
+fun CLASIMPSET' tacf i state = CLASET (fn cs => SIMPSET (fn ss => tacf (cs, ss) i)) state;
+
+
local
fun blast_depth_tac cs m i thm = Blast.depth_tac cs m i thm