Mon, 16 Jul 2007 21:17:12 +0200 | krauss | added lemma binding: accpI = accp.accI | file | diff | annotate |
Wed, 11 Jul 2007 11:00:09 +0200 | berghofe | acc is now defined using inductive_set. | file | diff | annotate |
Wed, 07 Feb 2007 17:28:09 +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, 17 May 2006 01:23:40 +0200 | wenzelm | tuned source/document; | 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 |