# HG changeset patch
# User wenzelm
# Date 894120377 -7200
# Node ID 7301ff9f412b226047248bbe710cc846a5686814
# Parent  bbc13af86c16d8d5a9a232c58e66a37ddc2db27e
added CLASIMPSET(') tacticals;

diff -r bbc13af86c16 -r 7301ff9f412b src/Provers/clasimp.ML
--- 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