2006-11-23 wenzelm 2006-11-23 declarations: pass morphism (dummy);
2006-11-21 wenzelm 2006-11-21 LocalTheory.axioms/notes/defs: proper kind; simplified Proof.theorem(_i);
2006-11-15 wenzelm 2006-11-15 replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
2006-11-14 wenzelm 2006-11-14 simplified Proof.theorem(_i) interface;
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 added profiling code, improved handling of proof terms, generation of domain introduction rules becomes optional (global reference FundefCommon.domintros)
2006-11-08 krauss 2006-11-08 Made "termination by lexicographic_order" the default for "fun" definitions.
2006-11-07 krauss 2006-11-07 untabified
2006-11-07 krauss 2006-11-07 Added datatype hook to declare all case_congs as "fundef_cong" automatically.
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-10-12 wenzelm 2006-10-12 Toplevel.local_theory_to_proof: proper target;
2006-10-07 wenzelm 2006-10-07 removed with_local_path -- LocalTheory.note admits qualified names; TheoryTarget.init;
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 Removed "induct set" attribute from total induction rules
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-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-08-04 krauss 2006-08-04 Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.
2006-08-03 wenzelm 2006-08-03 removed True_implies (cf. True_implies_equals);
2006-08-02 krauss 2006-08-02 Added type constraint to please sml/nj
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 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.