src/HOL/FunDef.thy
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Sat, 18 Feb 2012 09:46:58 +0100 krauss added congruence rules for Option.{map|bind}
Sat, 23 Oct 2010 23:42:04 +0200 krauss integrated partial_function into HOL-Plain
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Wed, 28 Apr 2010 11:52:04 +0200 krauss default termination prover as plain tactic
Sat, 02 Jan 2010 23:18:58 +0100 krauss absorb structures Decompose and Descent into Termination, to simplify further restructuring
Fri, 06 Nov 2009 14:42:42 +0100 krauss renamed method induct_scheme to induction_schema
Fri, 30 Oct 2009 01:32:06 +0100 krauss absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
Fri, 23 Oct 2009 16:37:56 +0200 krauss renamed auto_term.ML -> relation.ML
Fri, 23 Oct 2009 16:22:10 +0200 krauss function package: more standard names for structures and files
Fri, 23 Oct 2009 15:33:19 +0200 krauss renamed FundefDatatype -> Function_Fun
Fri, 23 Oct 2009 14:33:07 +0200 krauss pat_completeness gets its own file
Mon, 27 Jul 2009 21:47:41 +0200 krauss "more standard" argument order of relation composition (op O)
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Thu, 12 Mar 2009 21:29:04 +0100 wenzelm keep dead code fresh;
Wed, 11 Mar 2009 15:56:49 +0100 haftmann min_weak_def [code del]
Wed, 11 Mar 2009 08:45:46 +0100 haftmann explicitly delete some code equations
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID
Tue, 16 Dec 2008 19:24:55 +0100 wenzelm proper document antiquotations;
Tue, 16 Dec 2008 08:46:07 +0100 krauss method "sizechange" proves termination of functions; added more infrastructure for termination proofs
Thu, 19 Jun 2008 11:46:14 +0200 krauss generalized induct_scheme method to prove conditional induction schemes.
Mon, 12 May 2008 22:11:06 +0200 krauss Measure functions can now be declared via special rules, allowing for a
Fri, 25 Apr 2008 16:28:06 +0200 krauss * New attribute "termination_simp": Simp rules for termination proofs
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.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