src/HOL/blastdata.ML
changeset 11753 02b257ef0ee2
parent 10906 de95ba2760fe
child 13550 5a176b8dda84
equal deleted inserted replaced
11752:8941d8d15dc8 11753:02b257ef0ee2
    21   val contr_tac = Classical.contr_tac
    21   val contr_tac = Classical.contr_tac
    22   val dup_intr	= Classical.dup_intr
    22   val dup_intr	= Classical.dup_intr
    23   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    23   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    24   val claset	= Classical.claset
    24   val claset	= Classical.claset
    25   val rep_cs    = Classical.rep_cs
    25   val rep_cs    = Classical.rep_cs
    26   val atomize	= atomize_rules
       
    27   val cla_modifiers = Classical.cla_modifiers;
    26   val cla_modifiers = Classical.cla_modifiers;
    28   val cla_meth' = Classical.cla_meth'
    27   val cla_meth' = Classical.cla_meth'
    29   end;
    28   end;
    30 
    29 
    31 structure Blast = BlastFun(Blast_Data);
    30 structure Blast = BlastFun(Blast_Data);