src/HOL/Ord.ML
Mon, 20 Mar 2000 18:25:35 +0100 paulson tidied
Wed, 09 Feb 2000 11:42:26 +0100 paulson new thm order_less_imp_le
Mon, 22 Nov 1999 12:10:27 +0100 nipkow Added linord_less_split
Mon, 27 Sep 1999 10:25:10 +0200 paulson removed order-sorted theorems from the default claset
Mon, 06 Sep 1999 18:18:40 +0200 oheimb added theorems le_maxI1 and le_maxI2, also in claset
Fri, 09 Jul 1999 18:58:05 +0200 wenzelm mono: AddXI/Es;
Thu, 10 Jun 1999 10:50:19 +0200 paulson expandshort
Fri, 04 Jun 1999 19:58:06 +0200 wenzelm added order_le_less_trans, order_less_le_trans;
Thu, 15 Apr 1999 18:10:37 +0200 nipkow Added new thms.
Wed, 03 Mar 1999 11:15:18 +0100 paulson expandshort
Wed, 27 Jan 1999 17:11:39 +0100 nipkow arith_tac for min/max
Thu, 14 Jan 1999 13:18:09 +0100 nipkow More arith refinements.
Wed, 13 Jan 1999 12:16:34 +0100 nipkow Refined arithmetic.
Wed, 13 Jan 1999 08:41:28 +0100 nipkow Simplified arithmetic.
Sat, 09 Jan 1999 15:24:11 +0100 nipkow Refined arith tactic.
Mon, 19 Oct 1998 15:34:50 +0200 nipkow Addsimps [max_le_iff_conj];
Fri, 09 Oct 1998 11:10:59 +0200 paulson polymorphic versions of nat_neq_iff and nat_neqE
Wed, 23 Sep 1998 10:15:09 +0200 paulson a few new theorems
Thu, 10 Sep 1998 17:17:22 +0200 paulson Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands
Sun, 12 Jul 1998 11:49:17 +0200 wenzelm isatool expandshort;
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Fri, 20 Feb 1998 17:56:39 +0100 nipkow Congruence rules use == in premises now.
Thu, 05 Feb 1998 10:47:29 +0100 paulson New theorem order_eq_refl
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Fri, 11 Apr 1997 15:21:36 +0200 paulson Yet more fast_tac->blast_tac, and other tidying
Wed, 12 Feb 1997 18:53:59 +0100 nipkow New class "order" and accompanying changes.
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip