src/HOL/Tools/function_package/fundef_package.ML
2006-06-21 krauss 2006-06-21 Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
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-13 wenzelm 2006-06-13 tuned;
2006-06-06 krauss 2006-06-06 HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
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-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-05-11 krauss 2006-05-11 Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug" due to abbreviations
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-05-07 krauss 2006-05-07 function-package: Changed record usage to make sml/nj happy...
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.