# HG changeset patch
# User haftmann
# Date 1162826961 -3600
# Node ID 44b09f675a89e3323a087454d79c9694dd08907f
# Parent  42ee69856dd0f439a1785c778a72dfbeaf0272c2
dropped blastdata.ML

diff -r 42ee69856dd0 -r 44b09f675a89 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Mon Nov 06 16:28:37 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-structure Blast_Data = 
-struct
-  type claset = Classical.claset
-  val equality_name = "op ="
-  val not_name = "Not"
-  val notE = HOL.notE
-  val ccontr = HOL.ccontr
-  val contr_tac = Classical.contr_tac
-  val dup_intr = Classical.dup_intr
-  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
-  val claset	= Classical.claset
-  val rep_cs = Classical.rep_cs
-  val cla_modifiers = Classical.cla_modifiers
-  val cla_meth' = Classical.cla_meth'
-end;
-
-structure Blast = BlastFun(Blast_Data);