| Thu, 06 Nov 2008 11:52:50 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 06 Nov 2008 10:05:48 +0100 |
nipkow |
Added second tiling example.
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:14:51 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Tue, 26 Jun 2007 18:28:40 +0200 |
paulson |
simplified
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2005 00:00:20 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Fri, 05 Dec 2003 12:58:18 +0100 |
paulson |
stylistic changes
|
file |
diff |
annotate
|
| Tue, 13 Nov 2001 22:18:03 +0100 |
wenzelm |
tuned inductions;
|
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 20:09:10 +0200 |
wenzelm |
inductive: no collective atts;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 17:40:16 +0100 |
wenzelm |
Induct: converted some theories to new-style format;
|
file |
diff |
annotate
|
| Tue, 12 Sep 2000 10:27:16 +0200 |
paulson |
tidying and updating for revised Mutilated Chess Board article
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:41:49 +0200 |
paulson |
replacing "below" by "lessThan"
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:55:11 +0200 |
paulson |
modified for new simprocs
|
file |
diff |
annotate
|
| Mon, 27 Mar 2000 16:25:53 +0200 |
paulson |
simplified constant "colored"
|
file |
diff |
annotate
|
| Thu, 09 Mar 2000 18:27:18 +0100 |
paulson |
nicely tarted up Mutil
|
file |
diff |
annotate
|
| Sat, 04 Mar 2000 12:02:41 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 18 Nov 1998 15:10:46 +0100 |
paulson |
Finally removing "Compl" from HOL
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 10:47:16 +0200 |
paulson |
Tidying and simplification of declarations
|
file |
diff |
annotate
|
| Wed, 07 May 1997 12:50:26 +0200 |
paulson |
New directory to contain examples of (co)inductive definitions
|
file |
diff |
annotate
|