src/HOL/ex/Fundefs.thy
2011-09-20 krauss 2011-09-20 match types when applying mono_thm -- previous export generalizes type variables; added trivial regression test
2011-02-22 krauss 2011-02-22 dropped obsolete FIXMEs
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-10-26 krauss 2010-10-26 declare recursive equation as ".simps", in accordance with other packages
2010-10-25 krauss 2010-10-25 some partial_function examples
2010-09-28 krauss 2010-09-28 no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.
2010-04-21 krauss 2010-04-21 tolerate eta-variants in f_graph.cases (from inductive package); added test case;
2010-04-21 krauss 2010-04-21 simplified example
2008-10-14 nipkow 2008-10-14 added lemma
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.