| Wed, 02 Jan 2008 15:14:17 +0100 | haftmann | removed some legacy instantiations | file | diff | annotate |
| Tue, 18 Dec 2007 16:26:46 +0100 | wenzelm | tuned proofs, document; | file | diff | annotate |
| Mon, 17 Dec 2007 17:01:54 +0100 | nipkow | removed legacy proofs | file | diff | annotate |
| Mon, 10 Dec 2007 11:24:12 +0100 | haftmann | switched import from Main to List | file | diff | annotate |
| Thu, 06 Dec 2007 19:58:21 +0100 | nipkow | R&F: added sgn lemma | file | diff | annotate |
| Thu, 08 Nov 2007 20:52:27 +0100 | wenzelm | tuned presentation; | file | diff | annotate |
| Thu, 08 Nov 2007 20:09:17 +0100 | wenzelm | avoid implicit use of prems; | file | diff | annotate |
| Wed, 07 Nov 2007 03:51:17 +0100 | kleing | map and prefix | file | diff | annotate |
| Mon, 05 Nov 2007 22:51:16 +0100 | kleing | misc lemmas about prefix, postfix, and parallel | file | diff | annotate |
| Thu, 14 Jun 2007 23:04:39 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Tue, 05 Jun 2007 16:26:07 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Thu, 25 Jan 2007 09:32:37 +0100 | haftmann | made executable | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Sat, 11 Nov 2006 16:11:42 +0100 | wenzelm | tuned proofs; | file | diff | annotate |
| Thu, 16 Feb 2006 21:12:00 +0100 | wenzelm | new-style definitions/abbreviations; | file | diff | annotate |
| Sat, 21 Jan 2006 23:02:21 +0100 | wenzelm | tuned proofs; | file | diff | annotate |
| Fri, 25 Nov 2005 19:20:56 +0100 | wenzelm | tuned induct proofs; | file | diff | annotate |
| Wed, 31 Aug 2005 15:46:38 +0200 | wenzelm | reactivate postfix by change of syntax; | file | diff | annotate |
| Wed, 01 Dec 2004 18:11:50 +0100 | nipkow | Removed postfix >= because of new >= sugar | file | diff | annotate |
| Wed, 18 Aug 2004 11:09:40 +0200 | nipkow | import -> imports | file | diff | annotate |
| Mon, 16 Aug 2004 14:22:27 +0200 | nipkow | New theory header syntax. | file | diff | annotate |
| Mon, 21 Jun 2004 10:25:57 +0200 | kleing | Merged in license change from Isabelle2004 | file | diff | annotate |
| Thu, 06 May 2004 14:14:18 +0200 | wenzelm | tuned document; | file | diff | annotate |
| Mon, 12 Apr 2004 19:54:32 +0200 | oheimb | removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy | file | diff | annotate |
| Thu, 18 Dec 2003 08:20:36 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Sat, 01 Dec 2001 18:52:32 +0100 | wenzelm | renamed class "term" to "type" (actually "HOL.type"); | file | diff | annotate |
| Tue, 30 Oct 2001 17:37:25 +0100 | wenzelm | tuned induct proofs; | file | diff | annotate |
| Mon, 15 Oct 2001 20:34:44 +0200 | wenzelm | GPLed; | file | diff | annotate |
| Thu, 11 Jan 2001 19:37:46 +0100 | wenzelm | added strict_prefixI', strict_prefixE'; | file | diff | annotate |
| Wed, 22 Nov 2000 21:47:04 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 06 Nov 2000 22:56:07 +0100 | wenzelm | improved: 'induct' handle non-atomic goals; | file | diff | annotate |
| Fri, 03 Nov 2000 21:35:36 +0100 | wenzelm | proper setup of "parallel"; | file | diff | annotate |
| Wed, 25 Oct 2000 18:31:21 +0200 | wenzelm | "List prefixes" library theory (replaces old Lex/Prefix); | file | diff | annotate |