# HG changeset patch
# User paulson
# Date 859973403 -7200
# Node ID 6dde30a9e905db8561072f05a16ddec062879f64
# Parent  7d640451ae7d0b1719f744bd1cacfb53c656165d
Installation of blast_tac

diff -r 7d640451ae7d -r 6dde30a9e905 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Apr 02 11:27:47 1997 +0200
+++ b/src/HOL/cladata.ML	Wed Apr 02 11:30:03 1997 +0200
@@ -61,3 +61,21 @@
 
 claset := HOL_cs;
 
+
+(*** Applying BlastFun to create Blast_tac ***)
+structure Blast_Data = 
+  struct
+  type claset	= Classical.claset
+  val notE	= notE
+  val ccontr	= ccontr
+  val contr_tac = Classical.contr_tac
+  val dup_intr	= Classical.dup_intr
+  val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
+  val claset	= Classical.claset
+  val rep_claset = Classical.rep_claset
+  end;
+
+structure Blast = BlastFun(Blast_Data);
+
+val Blast_tac = Blast.Blast_tac
+and blast_tac = Blast.blast_tac;