| 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
|