src/FOL/blastdata.ML
changeset 10429 8820f787e61e
parent 9561 714ad541a133
child 10906 de95ba2760fe
equal deleted inserted replaced
10428:8f15fbce549f 10429:8820f787e61e
     8   val contr_tac = Cla.contr_tac
     8   val contr_tac = Cla.contr_tac
     9   val dup_intr	= Cla.dup_intr
     9   val dup_intr	= Cla.dup_intr
    10   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    10   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    11   val claset	= Cla.claset
    11   val claset	= Cla.claset
    12   val rep_cs    = Cla.rep_cs
    12   val rep_cs    = Cla.rep_cs
    13   val atomize	= thms "atomize"
    13   val atomize	= thms "atomize'"
    14   val cla_modifiers = Cla.cla_modifiers;
    14   val cla_modifiers = Cla.cla_modifiers;
    15   val cla_meth' = Cla.cla_meth'
    15   val cla_meth' = Cla.cla_meth'
    16   end;
    16   end;
    17 
    17 
    18 structure Blast = BlastFun(Blast_Data);
    18 structure Blast = BlastFun(Blast_Data);