oheimb [Wed, 12 Aug 1998 16:21:18 +0200] rev 5304
the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset
oheimb [Wed, 12 Aug 1998 16:20:49 +0200] rev 5303
renamed mk_meta_eq to meta_eq
oheimb [Wed, 12 Aug 1998 16:16:49 +0200] rev 5302
removed superfluous o_apply
oheimb [Wed, 12 Aug 1998 16:15:37 +0200] rev 5301
streamlined proofs with new hoare_conseq1, hoare_conseq2