src/FOL/blastdata.ML
changeset 32176 893614e2c35c
parent 32175 a89979440d2c
child 32177 bc02c5bfcb5b
     1.1 --- a/src/FOL/blastdata.ML	Fri Jul 24 21:18:05 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,19 +0,0 @@
     1.4 -
     1.5 -(*** Applying BlastFun to create blast_tac ***)
     1.6 -structure Blast_Data = 
     1.7 -  struct
     1.8 -  type claset	= Cla.claset
     1.9 -  val equality_name = @{const_name "op ="}
    1.10 -  val not_name = @{const_name Not}
    1.11 -  val notE	= @{thm notE}
    1.12 -  val ccontr	= @{thm ccontr}
    1.13 -  val contr_tac = Cla.contr_tac
    1.14 -  val dup_intr	= Cla.dup_intr
    1.15 -  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.16 -  val rep_cs = Cla.rep_cs
    1.17 -  val cla_modifiers = Cla.cla_modifiers;
    1.18 -  val cla_meth' = Cla.cla_meth'
    1.19 -  end;
    1.20 -
    1.21 -structure Blast = BlastFun(Blast_Data);
    1.22 -val blast_tac = Blast.blast_tac;