diff -r 669d0bc621e1 -r 58f9ca06b76b src/Provers/clasimp.ML
--- 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;