src/HOL/FunDef.thy
Fri, 07 Dec 2007 09:42:20 +0100 krauss experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
Thu, 06 Dec 2007 12:58:01 +0100 krauss load sum_tree.ML
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Thu, 09 Aug 2007 15:52:42 +0200 haftmann re-eliminated Option.thy
Tue, 07 Aug 2007 09:38:44 +0200 haftmann split off theory Option for benefit of code generator
Wed, 11 Jul 2007 11:03:11 +0200 berghofe Inserted definition of in_rel again (since member2 was removed).
Mon, 25 Jun 2007 12:16:27 +0200 krauss removed "sum_tools.ML" in favour of BalancedTree
Sat, 02 Jun 2007 15:28:38 +0200 krauss "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
Thu, 10 May 2007 10:21:48 +0200 haftmann explicit import of Datatype.thy due to hook bootstrap problem
Sun, 06 May 2007 21:49:23 +0200 haftmann tuned
Thu, 26 Apr 2007 16:39:10 +0200 wenzelm added header;
Tue, 10 Apr 2007 14:11:01 +0200 krauss Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
Thu, 15 Feb 2007 17:35:19 +0100 krauss changed termination goal to use object quantifier
Thu, 15 Feb 2007 12:14:34 +0100 krauss added congruence rule for function composition
Wed, 07 Feb 2007 17:37:59 +0100 berghofe - wfP has been moved to theory Wellfounded_Recursion
Mon, 22 Jan 2007 17:29:43 +0100 krauss * Preliminary implementation of tail recursion
Fri, 24 Nov 2006 13:44:51 +0100 krauss Lemma "fundef_default_value" uses predicate instead of set.
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Tue, 14 Nov 2006 22:16:54 +0100 wenzelm inductive2: canonical specification syntax;
Mon, 13 Nov 2006 13:51:22 +0100 krauss replaced "auto_term" by the simpler method "relation", which does not try
Sun, 12 Nov 2006 19:22:10 +0100 nipkow started reorgnization of lattice theories
Tue, 07 Nov 2006 11:53:55 +0100 krauss Preparations for making "lexicographic_order" part of "fun"
Wed, 18 Oct 2006 16:13:03 +0200 krauss Switched function package to use the new package for inductive predicates.
Thu, 21 Sep 2006 12:22:05 +0200 krauss 1. Function package accepts a parameter (default "some_term"), which specifies the functions
Thu, 14 Sep 2006 15:27:08 +0200 krauss Function package: Outside their domain functions now return "arbitrary".
Wed, 13 Sep 2006 12:05:50 +0200 krauss Major update to function package, including new syntax and the (only theoretical)
Thu, 03 Aug 2006 15:03:11 +0200 wenzelm removed True_implies (cf. True_implies_equals);
Mon, 31 Jul 2006 18:07:42 +0200 krauss Function package can now do automatic splits of overlapping datatype patterns
Wed, 21 Jun 2006 11:08:04 +0200 krauss Added split_cong rule
Mon, 05 Jun 2006 14:26:07 +0200 krauss HOL/Tools/function_package: Added support for mutual recursive definitions.
Fri, 05 May 2006 17:17:21 +0200 krauss First usable version of the new function definition package (HOL/function_packake/...).
less more (0) tip