src/HOL/ex/mesontest2.ML
2007-02-07 berghofe 2007-02-07 Renamed member to memb to avoid confusion with member function defined in Predicate theory.
2006-12-10 wenzelm 2006-12-10 avoid internal name O_;
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2005-05-20 paulson 2005-05-20 converted some problems to Isar format
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-11-22 nipkow 2004-11-22 fixed proof
2004-11-15 paulson 2004-11-15 Renamed some variables to eliminate conflicts with constants. Introduced some abbreviations (following TPTP axiom sets) to reduce the amount of repetition. Uncommented some examples, which increases the runtime somewhat.
2003-10-08 paulson 2003-10-08 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
2003-09-04 paulson 2003-09-04 quantifier symbols
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2000-11-10 wenzelm 2000-11-10 proper theory context for mesontest2;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-09-05 paulson 2000-09-05 safe_meson_tac -> meson_tac
2000-05-30 wenzelm 2000-05-30 cleaned up;
2000-03-23 paulson 2000-03-23 restored the MESON examples file HOL/ex/mesontest2.ML
1997-12-19 wenzelm 1997-12-19 tuned;
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1996-10-07 paulson 1996-10-07 New comment in header
1996-07-26 paulson 1996-07-26 Removed clash with "range" constant
1996-05-10 paulson 1996-05-10 Corrected and augmented timings
1996-05-06 paulson 1996-05-06 Updated timings; more theorems can be proved
1996-05-03 paulson 1996-05-03 Extra examples for safe_meson_tac