src/HOL/Tools/inductive_package.ML
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-18 wenzelm 2008-06-18 OldGoals.read_prop;
2008-05-24 wenzelm 2008-05-24 more uniform treatment of OuterSyntax.local_theory commands;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-22 haftmann 2008-04-22 added explicit check phase after reading of specification
2008-04-03 berghofe 2008-04-03 Added skip_mono flag and inductive_flags type.
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (turned into proper argument);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-25 wenzelm 2008-02-25 inductive package: simplified group handling;
2008-01-26 wenzelm 2008-01-26 added theorem group;
2008-01-03 berghofe 2008-01-03 Added function partition_rules'.
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-10 wenzelm 2007-11-10 put_inductives: be permissive about multiple versions (target names are not necessarily unique); add_inductive: store info under global (!) name -- very rough approximation of the real thing;
2007-11-09 wenzelm 2007-11-09 avoid obsolete Sign.read_prop;
2007-11-05 wenzelm 2007-11-05 improved error message for missing predicates;
2007-10-22 wenzelm 2007-10-22 abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
2007-10-20 wenzelm 2007-10-20 add_inductive: more careful handling of abbrevs -- do not expand prematurely;
2007-10-15 wenzelm 2007-10-15 tuned comment;
2007-10-14 wenzelm 2007-10-14 gen_add_inductive_i: treat abbrevs as local defs, expand by export; tuned;
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs, use plain LocalTheory.def;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-08 haftmann 2007-10-08 integrated FixedPoint into Inductive
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-10-02 wenzelm 2007-10-02 tuned internal interfaces: flags record, added kind for results; tuned;
2007-09-28 berghofe 2007-09-28 - add_inductive_i now takes typ instead of typ option as argument - close_rule is now applied before expanding abbreviations - rulify applies norm_hhf again
2007-09-26 wenzelm 2007-09-26 proper Specification.read_specification; Attrib.eval_thms;
2007-09-01 wenzelm 2007-09-01 removed obsolete ML bindings;
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
2007-08-02 wenzelm 2007-08-02 added int type constraints to accomodate hacked SML/NJ;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-07-11 berghofe 2007-07-11 Reorganization due to introduction of inductive_set wrapper.
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-15 berghofe 2007-05-15 Fixed bug that caused proof of induction theorem to fail if introduction rules contained True or False.
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-05-06 haftmann 2007-05-06 tuned
2007-04-25 berghofe 2007-04-25 Added functions arities_of, params_of, partition_rules, and infer_intro_vars (from inductive_realizer.ML).
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-14 wenzelm 2007-04-14 data declaration: removed obsolete target_morphism;
2007-04-05 berghofe 2007-04-05 - Removed occurrences of ProofContext.export in add_ind_def that caused theorems to end up in the wrong context - Explicit parameters are now generalized in theorems returned by add_inductive(_i)
2007-03-16 haftmann 2007-03-16 inf_fun_eq and inf_bool_eq now with meta equality
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-02-07 berghofe 2007-02-07 - Improved handling of monotonicity rules involving <= - ind_cases: variables to be generalized can now be specified using "for" keyword
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-12 wenzelm 2006-12-12 LocalTheory.abbrev;
2006-12-11 berghofe 2006-12-11 Abbreviations can now be specified simultaneously with introduction rules.
2006-12-05 wenzelm 2006-12-05 Attrib.internal: morphism;
2006-11-26 wenzelm 2006-11-26 added morh_result, the_inductive, add_inductive_global; removed get_inductive; more careful treatment of result naming/morphing;
2006-11-23 wenzelm 2006-11-23 more careful declaration of "inducts";
2006-11-23 wenzelm 2006-11-23 declarations: pass morphism (dummy);
2006-11-22 wenzelm 2006-11-22 more careful declaration of "intros" as Pure.intro;
2006-11-21 wenzelm 2006-11-21 LocalTheory.axioms/notes/defs: proper kind; context_notes: ProofContext.set_stmt after import;
2006-11-15 wenzelm 2006-11-15 replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; declared intro/elim rules;
2006-11-14 wenzelm 2006-11-14 inductive: canonical specification syntax (flattened result only); inductive_cases: local_theory; mk_cases/ind_cases: removed legacy code, proper treatment of fixed variables; get_inductive etc.: Proof.context; removed old trace/debug code; tuned;