changeset 9486 | 2df511ebb956 |
parent 7355 | 4c43090659ca |
child 9561 | 714ad541a133 |
--- a/src/FOL/blastdata.ML Tue Aug 01 11:55:27 2000 +0200 +++ b/src/FOL/blastdata.ML Tue Aug 01 11:57:09 2000 +0200 @@ -10,6 +10,7 @@ val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac val claset = Cla.claset val rep_cs = Cla.rep_cs + val atomize = [thm "all_eq", thm "imp_eq"] val cla_modifiers = Cla.cla_modifiers; val cla_meth' = Cla.cla_meth' end;