src/FOLP/simpdata.ML
2008-03-18 wenzelm 2008-03-18 converted legacy ML scripts;
2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
1998-08-12 oheimb 1998-08-12 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
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-02-10 paulson 1997-02-10 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-04-06 lcp 1995-04-06 No longer builds the induction structure (from ../Provers/ind.ML)
1993-09-16 clasohm 1993-09-16 Initial revision