| 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 |