Now builds blast_tac
authorpaulson
Wed, 02 Apr 1997 15:19:40 +0200
changeset 2867 0aa5a3cd4550
parent 2866 0a648ebbf6d4
child 2868 17a23a62f82a
Now builds blast_tac
src/FOL/cladata.ML
--- 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;
+
+