src/HOL/FunDef.thy
2013-09-08 Manuel Eberl 2013-09-08 generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)
2012-10-31 blanchet 2012-10-31 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-23 wenzelm 2012-04-23 more standard method setup;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-18 krauss 2012-02-18 added congruence rules for Option.{map|bind}
2010-10-23 krauss 2010-10-23 integrated partial_function into HOL-Plain
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-04-28 krauss 2010-04-28 default termination prover as plain tactic
2010-01-02 krauss 2010-01-02 absorb structures Decompose and Descent into Termination, to simplify further restructuring
2009-11-06 krauss 2009-11-06 renamed method induct_scheme to induction_schema
2009-10-30 krauss 2009-10-30 absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
2009-10-23 krauss 2009-10-23 renamed auto_term.ML -> relation.ML
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-10-23 krauss 2009-10-23 renamed FundefDatatype -> Function_Fun
2009-10-23 krauss 2009-10-23 pat_completeness gets its own file
2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-12 wenzelm 2009-03-12 keep dead code fresh;
2009-03-11 haftmann 2009-03-11 min_weak_def [code del]
2009-03-11 haftmann 2009-03-11 explicitly delete some code equations
2009-01-21 haftmann 2009-01-21 dropped ID
2008-12-16 wenzelm 2008-12-16 proper document antiquotations;
2008-12-16 krauss 2008-12-16 method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-06-19 krauss 2008-06-19 generalized induct_scheme method to prove conditional induction schemes.
2008-05-12 krauss 2008-05-12 Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.
2008-04-25 krauss 2008-04-25 * New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2007-12-07 krauss 2007-12-07 experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
2007-12-06 krauss 2007-12-06 load sum_tree.ML
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-08-09 haftmann 2007-08-09 re-eliminated Option.thy
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-07-11 berghofe 2007-07-11 Inserted definition of in_rel again (since member2 was removed).
2007-06-25 krauss 2007-06-25 removed "sum_tools.ML" in favour of BalancedTree
2007-06-02 krauss 2007-06-02 "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup.
2007-05-10 haftmann 2007-05-10 explicit import of Datatype.thy due to hook bootstrap problem
2007-05-06 haftmann 2007-05-06 tuned
2007-04-26 wenzelm 2007-04-26 added header; tuned presentation;
2007-04-10 krauss 2007-04-10 Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
2007-02-15 krauss 2007-02-15 changed termination goal to use object quantifier
2007-02-15 krauss 2007-02-15 added congruence rule for function composition
2007-02-07 berghofe 2007-02-07 - wfP has been moved to theory Wellfounded_Recursion - Accessible part now works on predicates, hence accP is no longer needed
2007-01-22 krauss 2007-01-22 * Preliminary implementation of tail recursion * Clarified internal interfaces
2006-11-24 krauss 2006-11-24 Lemma "fundef_default_value" uses predicate instead of set.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-14 wenzelm 2006-11-14 inductive2: canonical specification syntax;
2006-11-13 krauss 2006-11-13 replaced "auto_term" by the simpler method "relation", which does not try to simplify. Some more cleanup.
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
2006-11-07 krauss 2006-11-07 Preparations for making "lexicographic_order" part of "fun"
2006-10-18 krauss 2006-10-18 Switched function package to use the new package for inductive predicates.
2006-09-21 krauss 2006-09-21 1. Function package accepts a parameter (default "some_term"), which specifies the functions behaviour outside its domain. 2. Bugfix: An exception occured when a function in a mutual definition was declared but no equation was given.
2006-09-14 krauss 2006-09-14 Function package: Outside their domain functions now return "arbitrary".
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-08-03 wenzelm 2006-08-03 removed True_implies (cf. True_implies_equals); added header;
2006-07-31 krauss 2006-07-31 Function package can now do automatic splits of overlapping datatype patterns
2006-06-21 krauss 2006-06-21 Added split_cong rule
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.