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