--- a/src/Provers/clasimp.ML Wed Nov 18 11:00:02 1998 +0100
+++ b/src/Provers/clasimp.ML Wed Nov 18 11:01:48 1998 +0100
@@ -44,6 +44,7 @@
val force_tac : clasimpset -> int -> tactic
val Force_tac : int -> tactic
val force : int -> unit
+ val setup : (theory -> theory) list
end;
functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
@@ -146,4 +147,25 @@
fun force i = by (Force_tac i);
+(* methods *)
+
+fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
+
+val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
+val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
+
+fun clasimp_meth tac ctxt = Method.METHOD0 (tac (get_local_clasimpset ctxt));
+fun clasimp_meth' tac ctxt = Method.METHOD0 (FIRSTGOAL (tac (get_local_clasimpset ctxt)));
+
+val clasimp_method = clasimp_args o clasimp_meth;
+val clasimp_method' = clasimp_args o clasimp_meth';
+
+
+val setup =
+ [Method.add_methods
+ [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp"),
+ ("auto", clasimp_method auto_tac, "auto"),
+ ("force", clasimp_method' force_tac, "force")]];
+
+
end;