src/HOL/Tools/function_package/fundef_datatype.ML
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-08-28 krauss 2007-08-28 fixed pattern comnpletion; untabified
2007-08-20 krauss 2007-08-20 issue a warning, when encountering redundant equations (covered by prece3ding clauses)
2007-08-07 krauss 2007-08-07 more error handling
2007-07-16 krauss 2007-07-16 some interface cleanup
2007-06-13 wenzelm 2007-06-13 Method.Basic: include position;
2007-06-02 krauss 2007-06-02 "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup.
2007-06-01 krauss 2007-06-01 simplified interfaces, some restructuring
2007-05-21 krauss 2007-05-21 fixed signature
2007-05-09 krauss 2007-05-09 "fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"
2007-04-20 krauss 2007-04-20 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" do not depend on "termination" setup.
2007-03-22 krauss 2007-03-22 made function syntax strict, requiring | to separate equations; cleanup
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
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-08 krauss 2006-11-08 Made "termination by lexicographic_order" the default for "fun" definitions.
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-10-12 wenzelm 2006-10-12 Toplevel.local_theory: proper target; removed dead code;
2006-10-07 wenzelm 2006-10-07 TheoryTarget.init;
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-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-08-05 wenzelm 2006-08-05 avoid low-level tsig;
2006-06-19 krauss 2006-06-19 Fixed name clash. Function-goals are now fully quantified. Avoiding large meta-conjunctions when setting up the goal. Cleanup.
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.