| Mon, 28 Jun 2010 15:32:06 +0200 |
haftmann |
dropped ancient infix mem; refined code generation operations in List.thy
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 20:22:06 +0200 |
nipkow |
tuned set_replicate lemmas
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 16 Jun 2004 14:56:58 +0200 |
paulson |
new fib example
|
file |
diff |
annotate
|
| Wed, 22 Oct 2003 10:52:36 +0200 |
paulson |
InductiveInvariant_examples illustrates advanced recursive function definitions
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:33:54 +0100 |
wenzelm |
tuned;
|
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
|
| Thu, 01 Feb 2001 20:51:13 +0100 |
wenzelm |
converted to new-style theories;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2000 10:23:24 +0100 |
paulson |
deleted unnecessary "simpset" part from recdef
|
file |
diff |
annotate
|
| Fri, 10 Mar 2000 17:53:16 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 13:04:23 +0200 |
wenzelm |
recdef requires theory Recdef;
|
file |
diff |
annotate
|
| Tue, 20 Apr 1999 14:36:19 +0200 |
paulson |
Main is the correct parent
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 14:40:11 +0200 |
paulson |
new theorem less_Suc_eq_le
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 17:35:39 +0200 |
wenzelm |
stepping stones: Recdef, Main;
|
file |
diff |
annotate
|