src/HOL/Tools/inductive_package.ML
2006-02-03 ago canonical member/insert/merge;
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-26 ago Inductive sets with no introduction rules are now allowed as well.
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2006-01-10 ago generic attributes;
2005-12-22 ago actually produce projected rules;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
2005-12-06 ago re-oriented some result tuples in PureThy
2005-12-02 ago introduced new map2, fold
2005-11-23 ago RuleCases.case_conclusion;
2005-11-22 ago declare coinduct rule;
2005-10-25 ago avoid legacy goals;
2005-10-21 ago OldGoals;
2005-09-19 ago introduced AList module
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-12 ago introduced new-style AList operations
2005-09-05 ago curried_lookup/update;
2005-08-16 ago OuterKeyword;
2005-08-03 ago changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
2005-08-01 ago Sign.read_term;
2005-07-28 ago Sign.typ_unify;
2005-07-19 ago Logic.incr_tvar;
2005-07-15 ago tuned fold on terms;
2005-07-13 ago (corrected wrong commit)
2005-07-13 ago (intermediate commit)
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago refer to name spaces values instead of names;
2005-06-05 ago Type.freeze;
2005-05-31 ago renamed cond_extern to extern;
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-02-10 ago HOL.order -> Orderings.order due to restructering
2005-01-24 ago Adapted to modified interface of PureThy.get_thm(s).
2004-12-16 ago Further fix to a bug (involving equational premises) in inductive definitions
2004-12-09 ago converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
2004-07-11 ago local_cla/simpset_of;
2004-06-21 ago Merged in license change from Isabelle2004
2004-04-22 ago tuned;
2003-10-15 ago Fixed bug in mk_ind_def that caused the inductive definition package to
2002-12-12 ago Better treatment of equality in premises of inductive definitions. Less
2002-11-13 ago - No longer applies norm_hhf_rule
2002-10-21 ago Now applies standard' to "unfold" theorem (due to flex-flex constraints).
2002-10-04 ago Fixed bug involving inductive definitions having equalities in the premises,
2002-05-31 ago Changed interface of MetaSimplifier.rewrite_term.
2002-02-21 ago clarified internal theory dependencies;
2002-02-20 ago Symbol.bump_string;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-17 ago MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
2002-01-11 ago IsarThy.theorems_i;
2001-12-29 ago 'inductive_cases': support 'and' form;
2001-12-18 ago tuned Type.unify;
2001-12-14 ago changed Type.varify;