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