src/HOL/Tools/function_package/fundef_core.ML
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-01-02 krauss 2009-01-02 removed references to OldTerm.*
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-26 krauss 2008-08-26 function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies; Term.all;
2008-06-10 wenzelm 2008-06-10 eliminated obsolete case_split_thm -- use case_split;
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-07 wenzelm 2008-04-07 abs_conv: extra argument for bound variable;
2008-04-03 krauss 2008-04-03 Function package no longer overwrites theorems. Some tuning.
2008-03-05 krauss 2008-03-05 Use conversions instead of simplifier. tuned
2008-02-22 krauss 2008-02-22 removed dead code; some cleanup
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-11 wenzelm 2007-10-11 replaced (flip Thm.implies_elim) by Thm.elim_implies;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-09-24 wenzelm 2007-09-24 eliminated ProofContext.read_termTs;
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
2007-08-07 krauss 2007-08-07 simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"
2007-07-20 haftmann 2007-07-20 dropped Nat.ML legacy bindings
2007-07-16 krauss 2007-07-16 some interface cleanup
2007-07-11 berghofe 2007-07-11 Adapted to changes in Accessible_Part theory.
2007-06-01 krauss 2007-06-01 simplified interfaces, some restructuring
2007-04-23 wenzelm 2007-04-23 simplified ProofContext.read_termTs;
2007-04-20 krauss 2007-04-20 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" do not depend on "termination" setup.
2007-04-10 krauss 2007-04-10 removed obsolete workaround
2007-03-22 krauss 2007-03-22 cleanup
2007-03-16 haftmann 2007-03-16 adjusted qualified thm reference
2007-03-06 krauss 2007-03-06 fixed function package bug in the handling of multiple guards
2007-02-15 krauss 2007-02-15 changed termination goal to use object quantifier
2007-02-07 berghofe 2007-02-07 Adapted to changes in Accessible_Part and Wellfounded_Recursion theories.
2007-01-22 krauss 2007-01-22 * Preliminary implementation of tail recursion * Clarified internal interfaces