src/HOL/Tools/function_package/fundef_package.ML
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.
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