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