| Sat, 30 Sep 2006 21:39:25 +0200 | wenzelm | proper import of Main HOL; | file | diff | annotate |
| Thu, 28 Sep 2006 23:42:43 +0200 | wenzelm | fixed translations: CONST; | file | diff | annotate |
| Sat, 27 May 2006 17:42:02 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 12 Oct 2005 10:49:07 +0200 | paulson | tidying | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Mon, 09 May 2005 16:38:56 +0200 | paulson | from simplesubst to new subst | file | diff | annotate |
| Tue, 01 Feb 2005 18:01:57 +0100 | paulson | the new subst tactic, by Lucas Dixon | file | diff | annotate |
| Wed, 15 Dec 2004 17:32:40 +0100 | paulson | removal of archaic Abs/Rep proofs | file | diff | annotate |
| Thu, 26 Sep 2002 10:51:29 +0200 | paulson | Converted Fun to Isar style. | file | diff | annotate |
| Tue, 27 Aug 2002 11:03:05 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Tue, 07 May 2002 14:27:39 +0200 | wenzelm | tuned presentation; | file | diff | annotate |
| Tue, 02 Apr 2002 14:28:28 +0200 | paulson | conversion of some HOL/Induct proof scripts to Isar | file | diff | annotate |
| Tue, 09 Jan 2001 15:32:27 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Wed, 17 Mar 1999 13:47:34 +0100 | wenzelm | fixed typedef representing set; | file | diff | annotate |
| Thu, 26 Nov 1998 17:40:10 +0100 | paulson | tidied up list definitions, using type 'a option instead of | file | diff | annotate |
| Fri, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | file | diff | annotate |
| Wed, 07 May 1997 12:50:26 +0200 | paulson | New directory to contain examples of (co)inductive definitions | file | diff | annotate |