src/HOL/Tools/inductive_package.ML
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;
2006-11-14 wenzelm 2006-11-14 incorporated IsarThy into IsarCmd;
2006-10-17 berghofe 2006-10-17 Restructured and repaired code dealing with case names in induction and elimination rules.
2006-10-13 berghofe 2006-10-13 Completely rewrote inductive definition package. Now allows to define n-ary predicates directly (rather than sets of n-tuples), using generalized fixpoint theory for arbitrary complete lattices.
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping; PureThy.note_thmss_i;
2006-10-07 wenzelm 2006-10-07 tuned;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-29 wenzelm 2006-07-29 Goal.prove: more tactic arguments;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 Goal.prove_global; SkipProof.prove: context;
2006-06-13 wenzelm 2006-06-13 ProjectRule now context dependent;
2006-04-07 berghofe 2006-04-07 Fixed bug that caused proof of induction rule to fail for inductive sets with trivial introduction rules such as "x : S ==> x : S".
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-26 berghofe 2006-01-26 Inductive sets with no introduction rules are now allowed as well.