changeset 9530 | f0ffd29fd4e4 |
parent 9486 | 2df511ebb956 |
child 10429 | 8820f787e61e |
--- a/src/HOL/blastdata.ML Fri Aug 04 22:56:52 2000 +0200 +++ b/src/HOL/blastdata.ML Fri Aug 04 22:57:25 2000 +0200 @@ -23,7 +23,7 @@ val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac val claset = Classical.claset val rep_cs = Classical.rep_cs - val atomize = [thm "all_eq", thm "imp_eq"] + val atomize = thms "atomize" val cla_modifiers = Classical.cla_modifiers; val cla_meth' = Classical.cla_meth' end;