src/FOL/cladata.ML
changeset 7156 3e84e73a3b6a
parent 5929 890f2f9b926d
child 7355 4c43090659ca
equal deleted inserted replaced
7155:70ba7d640bfe 7156:3e84e73a3b6a
    56   val contr_tac = Cla.contr_tac
    56   val contr_tac = Cla.contr_tac
    57   val dup_intr	= Cla.dup_intr
    57   val dup_intr	= Cla.dup_intr
    58   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    58   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    59   val claset	= Cla.claset
    59   val claset	= Cla.claset
    60   val rep_cs    = Cla.rep_cs
    60   val rep_cs    = Cla.rep_cs
    61   val cla_method' = Cla.cla_method'
    61   val cla_modifiers = Cla.cla_modifiers;
       
    62   val cla_meth' = Cla.cla_meth'
    62   end;
    63   end;
    63 
    64 
    64 structure Blast = BlastFun(Blast_Data);
    65 structure Blast = BlastFun(Blast_Data);
    65 
    66 
    66 val Blast_tac = Blast.Blast_tac
    67 val Blast_tac = Blast.Blast_tac