src/Provers/blast.ML

 		 hazIs: thm list, hazEs: thm list,
 		 swrappers: (string * wrapper) list, 
 		 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;
 
 
 signature BLAST =
   sig

   type branch
   val depth_tac 	: claset -> int -> int -> tactic
   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
   val fullTrace	        : branch list list ref
   val fromType	        : (indexname * term) list ref -> Term.typ -> term

 		   Data.claset(), 
 		   [initBranch ([readGoal (sign_of thy) s], lim)], 
 		   I));
 
 
+(** method setup **)
+
+val setup = [Method.add_methods [("blast", Data.cla_method' blast_tac, "blast")]];
+
+
 end;