src/HOL/ex/Fundefs.thy
Tue, 20 Sep 2011 01:32:04 +0200 krauss match types when applying mono_thm -- previous export generalizes type variables;
Tue, 22 Feb 2011 16:47:18 +0100 krauss dropped obsolete FIXMEs
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Tue, 26 Oct 2010 12:19:01 +0200 krauss declare recursive equation as ".simps", in accordance with other packages
Mon, 25 Oct 2010 10:45:22 +0200 krauss some partial_function examples
Tue, 28 Sep 2010 09:54:07 +0200 krauss no longer declare .psimps rules as [simp].
Wed, 21 Apr 2010 15:45:33 +0200 krauss tolerate eta-variants in f_graph.cases (from inductive package); added test case;
Wed, 21 Apr 2010 15:37:39 +0200 krauss simplified example
Tue, 14 Oct 2008 13:24:07 +0200 nipkow added lemma
Mon, 17 Dec 2007 18:38:28 +0100 berghofe Adapted to changes in size function.
Wed, 24 Oct 2007 18:32:53 +0200 krauss tuned
Sat, 15 Sep 2007 19:27:40 +0200 haftmann tuned
Mon, 16 Jul 2007 21:16:16 +0200 krauss updated
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