| Wed, 07 Feb 2007 17:44:07 +0100 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Wed, 15 Nov 2006 16:23:55 +0100 | urbanc | replaced exists_fresh lemma with a version formulated with obtains; | file | diff | annotate |
| Mon, 30 Oct 2006 13:07:51 +0100 | urbanc | new file for defining functions in the lambda-calculus | file | diff | annotate |
| Sun, 02 Jul 2006 17:27:10 +0200 | urbanc | added more infrastructure for the recursion combinator | file | diff | annotate |
| Sat, 20 May 2006 23:36:56 +0200 | wenzelm | primrec (unchecked); | file | diff | annotate |
| Fri, 05 May 2006 17:17:21 +0200 | krauss | First usable version of the new function definition package (HOL/function_packake/...). | file | diff | annotate |