src/HOL/cladata.ML
changeset 2860 6dde30a9e905
parent 1985 84cf16192e03
child 2882 2563063772d9
     1.1 --- a/src/HOL/cladata.ML	Wed Apr 02 11:27:47 1997 +0200
     1.2 +++ b/src/HOL/cladata.ML	Wed Apr 02 11:30:03 1997 +0200
     1.3 @@ -61,3 +61,21 @@
     1.4  
     1.5  claset := HOL_cs;
     1.6  
     1.7 +
     1.8 +(*** Applying BlastFun to create Blast_tac ***)
     1.9 +structure Blast_Data = 
    1.10 +  struct
    1.11 +  type claset	= Classical.claset
    1.12 +  val notE	= notE
    1.13 +  val ccontr	= ccontr
    1.14 +  val contr_tac = Classical.contr_tac
    1.15 +  val dup_intr	= Classical.dup_intr
    1.16 +  val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
    1.17 +  val claset	= Classical.claset
    1.18 +  val rep_claset = Classical.rep_claset
    1.19 +  end;
    1.20 +
    1.21 +structure Blast = BlastFun(Blast_Data);
    1.22 +
    1.23 +val Blast_tac = Blast.Blast_tac
    1.24 +and blast_tac = Blast.blast_tac;