src/HOL/ex/Fundefs.thy
Mon, 11 Jun 2007 11:06:04 +0200 chaieb tuned Proof
Tue, 29 May 2007 14:03:49 +0200 krauss updated examples to include an instance of (lexicographic_order simp:...)
Wed, 18 Apr 2007 11:47:08 +0200 krauss proper header, added regression tests
Tue, 10 Apr 2007 08:19:20 +0200 krauss added example for definitions in local contexts
Wed, 21 Mar 2007 16:06:15 +0100 krauss Unified function syntax
Mon, 22 Jan 2007 17:29:43 +0100 krauss * Preliminary implementation of tail recursion
Mon, 13 Nov 2006 13:51:22 +0100 krauss replaced "auto_term" by the simpler method "relation", which does not try
Wed, 08 Nov 2006 09:08:54 +0100 krauss Made "termination by lexicographic_order" the default for "fun" definitions.
Wed, 18 Oct 2006 16:13:03 +0200 krauss Switched function package to use the new package for inductive predicates.
Thu, 14 Sep 2006 15:27:08 +0200 krauss Function package: Outside their domain functions now return "arbitrary".
Wed, 13 Sep 2006 12:37:13 +0200 krauss Removed debugging code imports...
Wed, 13 Sep 2006 12:05:50 +0200 krauss Major update to function package, including new syntax and the (only theoretical)
Mon, 31 Jul 2006 18:07:42 +0200 krauss Function package can now do automatic splits of overlapping datatype patterns
Mon, 19 Jun 2006 18:25:34 +0200 krauss Fixed name clash.
Tue, 06 Jun 2006 09:28:24 +0200 krauss HOL/Tools/function_package: imporoved handling of guards, added an example
Mon, 05 Jun 2006 14:26:07 +0200 krauss HOL/Tools/function_package: Added support for mutual recursive definitions.
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Sun, 07 May 2006 00:00:13 +0200 krauss function-package: Changed record usage to make sml/nj happy...
Fri, 05 May 2006 18:39:16 +0200 krauss Added small example theory for new function package.
less more (0) tip