src/HOL/ex/Fundefs.thy
2007-12-17 berghofe 2007-12-17 Adapted to changes in size function.
2007-10-24 krauss 2007-10-24 tuned
2007-09-15 haftmann 2007-09-15 tuned
2007-07-16 krauss 2007-07-16 updated
2007-06-11 chaieb 2007-06-11 tuned Proof
2007-05-29 krauss 2007-05-29 updated examples to include an instance of (lexicographic_order simp:...)
2007-04-18 krauss 2007-04-18 proper header, added regression tests
2007-04-10 krauss 2007-04-10 added example for definitions in local contexts
2007-03-21 krauss 2007-03-21 Unified function syntax
2007-01-22 krauss 2007-01-22 * Preliminary implementation of tail recursion * Clarified internal interfaces
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-10-18 krauss 2006-10-18 Switched function package to use the new package for inductive predicates.
2006-09-14 krauss 2006-09-14 Function package: Outside their domain functions now return "arbitrary".
2006-09-13 krauss 2006-09-13 Removed debugging code imports...
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-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: imporoved handling of guards, added an example
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-05-27 wenzelm 2006-05-27 tuned;
2006-05-07 krauss 2006-05-07 function-package: Changed record usage to make sml/nj happy...
2006-05-05 krauss 2006-05-05 Added small example theory for new function package.