src/HOL/Tools/function_package/pattern_split.ML
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-20 krauss 2006-09-20 Fixed error in pattern splitting algorithm
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-05 wenzelm 2006-08-05 avoid low-level tsig;
2006-08-04 krauss 2006-08-04 Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.
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