--- a/src/FOL/cladata.ML Wed Apr 02 15:18:21 1997 +0200
+++ b/src/FOL/cladata.ML Wed Apr 02 15:19:40 1997 +0200
@@ -7,7 +7,6 @@
*)
-(** Applying HypsubstFun to generate hyp_subst_tac **)
section "Classical Reasoner";
@@ -62,3 +61,22 @@
claset := FOL_cs;
+(*** Applying BlastFun to create Blast_tac ***)
+structure Blast_Data =
+ struct
+ type claset = Cla.claset
+ val notE = notE
+ val ccontr = ccontr
+ val contr_tac = Cla.contr_tac
+ val dup_intr = Cla.dup_intr
+ val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
+ val claset = Cla.claset
+ val rep_claset = Cla.rep_claset
+ end;
+
+structure Blast = BlastFun(Blast_Data);
+
+val Blast_tac = Blast.Blast_tac
+and blast_tac = Blast.blast_tac;
+
+