src/HOL/Tools/function_package/fundef_package.ML
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
2009-02-09 blanchet 2009-02-09 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.
2009-02-06 blanchet 2009-02-06 Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-11 krauss 2008-12-11 constrain type inference to sort "type"
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-05-24 wenzelm 2008-05-24 uniform treatment of target, not as config;
2008-04-25 krauss 2008-04-25 * New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-09 wenzelm 2008-04-09 fundef_afterqed: removed unused config, added do_print flag; print_consts only for external specifications;
2008-04-08 krauss 2008-04-08 Generic conversion and tactic "atomize_elim" to convert elimination rules to the object logic
2008-04-03 krauss 2008-04-03 Function package no longer overwrites theorems. Some tuning.
2008-02-27 wenzelm 2008-02-27 more precise handling of "group" for termination;
2008-02-25 wenzelm 2008-02-25 LocalTheory.set_group for user command;
2007-10-29 krauss 2007-10-29 fun/function: generate case names for induction rules
2007-10-26 krauss 2007-10-26 print the defined constants when finished; tuned
2007-10-24 krauss 2007-10-24 fun command: use "reinit" between "function" and "termination"
2007-10-18 krauss 2007-10-18 Simultaneous type inference using read_specification
2007-10-16 krauss 2007-10-16 "sequential" is no longer a keyword. It is still used as before, but as a normal identifier => no pollution of keyword space
2007-10-11 wenzelm 2007-10-11 replaced (flip Thm.implies_elim) by Thm.elim_implies;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 tuned Induct interface: prefer pred'' over set'';
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-26 wenzelm 2007-09-26 minimal adaptions for Specification.read/check_specification;
2007-09-25 wenzelm 2007-09-25 simplified interpretation setup;
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-07 krauss 2007-08-07 simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-16 krauss 2007-07-16 some interface cleanup
2007-06-22 krauss 2007-06-22 new method "elim_to_cases" provides ad-hoc conversion of obtain-style elimination goals to a disjunction of existentials.
2007-06-02 krauss 2007-06-02 "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup.
2007-06-01 krauss 2007-06-01 simplified interfaces, some restructuring
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
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-18 krauss 2007-04-18 added temporary hack to avoid schematic goals in "termination".
2007-04-14 wenzelm 2007-04-14 data declaration: removed obsolete target_morphism (still required for local data!?);
2007-04-11 krauss 2007-04-11 removed debugging code
2007-04-10 krauss 2007-04-10 proper handling of morphisms
2007-03-22 krauss 2007-03-22 made function syntax strict, requiring | to separate equations; cleanup
2007-02-15 krauss 2007-02-15 changed termination goal to use object quantifier
2007-01-23 krauss 2007-01-23 fixes smlnj-related problem, updated signature
2007-01-22 krauss 2007-01-22 * Preliminary implementation of tail recursion * Clarified internal interfaces
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;
2006-12-05 wenzelm 2006-12-05 Attrib.internal: morphism;
2006-11-30 wenzelm 2006-11-30 Goal.norm/close_result;
2006-11-24 krauss 2006-11-24 The function package declares the [code] attribute automatically again.
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.