src/HOL/Tools/inductive_package.ML
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;
2001-12-06 ago added the_mk_cases;
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-21 ago Set.vimage;
2001-11-14 ago inductive: removed con_defs;
2001-11-13 ago tuned;
2001-11-12 ago mutual rules declared as ``consumes 0'';
2001-11-09 ago tuned;
2001-11-08 ago theory data: finish method;
2001-10-31 ago use HOL.induct_XXX;
2001-10-22 ago quick_and_dirty_prove_goalw_cterm;
2001-10-18 ago GPLed;
2001-10-18 ago moved atomize stuff to theory HOL;
2001-10-15 ago Tactic.rewrite_cterm;
2001-10-14 ago moved rulify to ObjectLogic;
2001-10-14 ago "HOL.mono";
2001-10-13 ago IsarThy.theorem_i Drule.internalK;
2001-10-04 ago simp_case_tac is back again from induct_method.ML;
2001-09-28 ago inductive: no collective atts;
2001-08-16 ago prefer immediate monos;
2001-06-01 ago now checks for leading meta-quantifiers and complains, instead of
2001-02-02 ago use hol_simplify;
2001-01-31 ago more robust handling of rule cases hints;
2001-01-29 ago Splitting of arguments of product types in induction rules is now less
2001-01-16 ago export inductive_forall_name, inductive_forall_def, rulify;
2001-01-06 ago Tactic.norm_hhf;
2000-12-27 ago Method.erule 0;
2000-12-23 ago simplified quick_and_dirty stuff;
2000-12-22 ago handle proper rules;
2000-12-01 ago ignore quick_and_dirty for coind;
2000-10-19 ago InductAttrib;
2000-10-12 ago *** empty log message ***
2000-10-12 ago induct -> lfp_induct
2000-10-11 ago *** empty log message ***
2000-09-23 ago renaming the inverse image operator in HOL
2000-09-17 ago Display.pretty_thm_sg;
2000-09-12 ago tuned handling of "intros";