method setup;

--- a/src/Provers/blast.ML	Wed Nov 18 11:00:02 1998 +0100
+++ b/src/Provers/blast.ML	Wed Nov 18 11:01:48 1998 +0100
@@ -66,6 +66,7 @@
 		 uwrappers: (string * wrapper) list,
 		 safe0_netpair: netpair, safep_netpair: netpair,
 		 haz_netpair: netpair, dup_netpair: netpair}
+  val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   end;
 
 
@@ -87,6 +88,7 @@
   val blast_tac 	: claset -> int -> tactic
   val Blast_tac 	: int -> tactic
   val overloaded 	: string * (Term.typ -> Term.typ) -> unit
+  val setup		: (theory -> theory) list
   (*debugging tools*)
   val stats	        : bool ref
   val trace	        : bool ref
@@ -1322,4 +1324,9 @@
 		   I));
 
 
+(** method setup **)
+
+val setup = [Method.add_methods [("blast", Data.cla_method' blast_tac, "blast")]];
+
+
 end;

--- 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;