| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Sun, 01 Oct 2006 18:29:23 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 05 Jun 2006 14:22:58 +0200 | krauss | Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". | file | diff | annotate |
| Sat, 27 May 2006 17:42:02 +0200 | wenzelm | tuned; | file | diff | annotate |
| Thu, 08 Dec 2005 20:15:50 +0100 | wenzelm | tuned proofs; | file | diff | annotate |
| Fri, 10 Sep 2004 20:04:14 +0200 | nipkow | Added antisymmetry simproc | 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 |
| Thu, 06 May 2004 14:14:18 +0200 | wenzelm | tuned document; | file | diff | annotate |
| Fri, 16 Apr 2004 13:51:04 +0200 | wenzelm | tuned document; | file | diff | annotate |
| Thu, 18 Dec 2003 08:20:36 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Thu, 17 Jan 2002 15:06:36 +0100 | kleing | registered directly executable version with the code generator | file | diff | annotate |
| Tue, 23 Oct 2001 22:58:15 +0200 | wenzelm | eliminated old numerals; | file | diff | annotate |
| Sat, 06 Oct 2001 00:02:46 +0200 | wenzelm | * sane numerals (stage 2): plain "num" syntax (removed "#"); | file | diff | annotate |
| Fri, 05 Oct 2001 21:52:39 +0200 | wenzelm | sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, | file | diff | annotate |
| Fri, 28 Sep 2001 19:17:01 +0200 | wenzelm | recdef (permissive); | file | diff | annotate |
| Tue, 04 Sep 2001 21:10:57 +0200 | wenzelm | renamed "antecedent" case to "rule_context"; | file | diff | annotate |
| Fri, 04 May 2001 15:38:48 +0200 | nipkow | made same_fst recdef_simp | file | diff | annotate |
| Sat, 03 Feb 2001 17:43:05 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 29 Jan 2001 23:54:56 +0100 | wenzelm | avoid dead code; | file | diff | annotate |
| Fri, 26 Jan 2001 15:50:52 +0100 | nipkow | Merged Example into While_Combi | file | diff | annotate |
| Wed, 03 Jan 2001 21:24:29 +0100 | wenzelm | recdef_tc; | file | diff | annotate |
| Thu, 14 Dec 2000 19:37:27 +0100 | wenzelm | unsymbolize; | file | diff | annotate |
| Wed, 13 Dec 2000 09:32:55 +0100 | nipkow | small mods. | file | diff | annotate |
| Thu, 19 Oct 2000 01:48:26 +0200 | wenzelm | use RecdefPackage.tcs_of; | file | diff | annotate |
| Wed, 18 Oct 2000 23:29:49 +0200 | wenzelm | A general ``while'' combinator (from main HOL); | file | diff | annotate |