src/HOL/Tools/function_package/fundef_common.ML
2007-06-01 krauss 2007-06-01 simplified interfaces, some restructuring
2007-05-10 wenzelm 2007-05-10 Thm.match;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-20 haftmann 2007-04-20 repaired value restriction problem
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-04-10 krauss 2007-04-10 proper handling of morphisms
2007-03-22 krauss 2007-03-22 made function syntax strict, requiring | to separate equations; cleanup
2007-02-07 berghofe 2007-02-07 Adapted to changes in Accessible_Part and Wellfounded_Recursion theories.
2007-01-22 krauss 2007-01-22 * Preliminary implementation of tail recursion * Clarified internal interfaces
2006-12-13 haftmann 2006-12-13 whitespace correction
2006-11-14 haftmann 2006-11-14 value restriction
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 added profiling code, improved handling of proof terms, generation of domain introduction rules becomes optional (global reference FundefCommon.domintros)
2006-11-07 krauss 2006-11-07 untabified
2006-10-18 krauss 2006-10-18 Switched function package to use the new package for inductive predicates.
2006-10-07 wenzelm 2006-10-07 tuned comments;
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-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-31 krauss 2006-07-31 Function package can now do automatic splits of overlapping datatype patterns
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-06 krauss 2006-06-06 HOL/Tools/function_package: More cleanup
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-05-11 wenzelm 2006-05-11 use IntGraph from Pure;
2006-05-07 krauss 2006-05-07 function-package: Changed record usage to make sml/nj happy...
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.