| Tue, 05 Oct 1999 15:25:52 +0200 | berghofe | Additional rules for inductive package. | file | diff | annotate |
| Tue, 27 Jul 1999 22:04:54 +0200 | wenzelm | fixed comments; | file | diff | annotate |
| Fri, 23 Jul 1999 12:10:42 +0200 | nipkow | New lemmas by Stefan Merz. | file | diff | annotate |
| Tue, 15 Sep 1998 15:04:07 +0200 | paulson | From Compl(A) to -A | file | diff | annotate |
| Thu, 13 Aug 1998 18:14:26 +0200 | paulson | even more tidying of Goal commands | file | diff | annotate |
| Tue, 30 Jun 1998 20:49:49 +0200 | berghofe | Removed obsolete comments. | file | diff | annotate |
| Wed, 05 Nov 1997 13:32:07 +0100 | paulson | UNIV now a constant; UNION1, INTER1 now translations and no longer have | file | diff | annotate |
| Mon, 03 Nov 1997 12:13:18 +0100 | wenzelm | isatool fixclasimp; | file | diff | annotate |
| Fri, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | file | diff | annotate |
| Wed, 09 Apr 1997 12:32:04 +0200 | paulson | Using Blast_tac | file | diff | annotate |
| Thu, 11 Jul 1996 15:14:41 +0200 | paulson | Added insert_mono | file | diff | annotate |
| Thu, 23 May 1996 14:37:06 +0200 | berghofe | Replaced fast_tac by Fast_tac (which uses default claset) | file | diff | annotate |
| Mon, 19 Feb 1996 18:04:41 +0100 | nipkow | Introduced normalize_thm into HOL.ML | file | diff | annotate |
| Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Wed, 04 Oct 1995 13:10:03 +0100 | clasohm | added local simpsets; removed IOA from 'make test' | file | diff | annotate |
| Fri, 03 Mar 1995 12:02:25 +0100 | clasohm | new version of HOL with curried function application | file | diff | annotate |