src/FOL/blastdata.ML
changeset 32176 893614e2c35c
parent 32175 a89979440d2c
child 32177 bc02c5bfcb5b
equal deleted inserted replaced
32175:a89979440d2c 32176:893614e2c35c
     1 
       
     2 (*** Applying BlastFun to create blast_tac ***)
       
     3 structure Blast_Data = 
       
     4   struct
       
     5   type claset	= Cla.claset
       
     6   val equality_name = @{const_name "op ="}
       
     7   val not_name = @{const_name Not}
       
     8   val notE	= @{thm notE}
       
     9   val ccontr	= @{thm ccontr}
       
    10   val contr_tac = Cla.contr_tac
       
    11   val dup_intr	= Cla.dup_intr
       
    12   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
       
    13   val rep_cs = Cla.rep_cs
       
    14   val cla_modifiers = Cla.cla_modifiers;
       
    15   val cla_meth' = Cla.cla_meth'
       
    16   end;
       
    17 
       
    18 structure Blast = BlastFun(Blast_Data);
       
    19 val blast_tac = Blast.blast_tac;