src/HOL/Ord.ML
1999-03-03 paulson 1999-03-03 expandshort
1999-01-27 nipkow 1999-01-27 arith_tac for min/max
1999-01-14 nipkow 1999-01-14 More arith refinements.
1999-01-13 nipkow 1999-01-13 Refined arithmetic.
1999-01-13 nipkow 1999-01-13 Simplified arithmetic.
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1998-10-19 nipkow 1998-10-19 Addsimps [max_le_iff_conj]; Addsimps [le_min_iff_conj];
1998-10-09 paulson 1998-10-09 polymorphic versions of nat_neq_iff and nat_neqE
1998-09-23 paulson 1998-09-23 a few new theorems
1998-09-10 paulson 1998-09-10 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-07-12 wenzelm 1998-07-12 isatool expandshort;
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now. New class linord.
1998-02-05 paulson 1998-02-05 New theorem order_eq_refl
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application