src/HOL/Tools/inductive_package.ML
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.
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-10 wenzelm 2006-01-10 generic attributes;
2005-12-22 wenzelm 2005-12-22 actually produce projected rules; *.inducts holds all projected rules;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-12-02 haftmann 2005-12-02 introduced new map2, fold
2005-11-23 wenzelm 2005-11-23 RuleCases.case_conclusion;
2005-11-22 wenzelm 2005-11-22 declare coinduct rule; tuned;
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-19 haftmann 2005-09-19 introduced AList module
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-03 avigad 2005-08-03 changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
2005-08-01 wenzelm 2005-08-01 Sign.read_term;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify;
2005-07-19 wenzelm 2005-07-19 Logic.incr_tvar;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-13 haftmann 2005-07-13 (corrected wrong commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Context.theory_name;
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-06-05 wenzelm 2005-06-05 Type.freeze;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-10 nipkow 2005-02-10 HOL.order -> Orderings.order due to restructering
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-12-16 paulson 2004-12-16 Further fix to a bug (involving equational premises) in inductive definitions
2004-12-09 paulson 2004-12-09 converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global