src/HOL/FunDef.thy
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.