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.
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.