src/HOL/Tools/inductive_package.ML
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
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-04-22 wenzelm 2004-04-22 tuned;
2003-10-15 berghofe 2003-10-15 Fixed bug in mk_ind_def that caused the inductive definition package to crash in cases where the declaration of a constant and its definition were located in different theory files.
2002-12-12 paulson 2002-12-12 Better treatment of equality in premises of inductive definitions. Less backtracking.
2002-11-13 berghofe 2002-11-13 - No longer applies norm_hhf_rule - intrs field now contains theorems with names specified by user
2002-10-21 berghofe 2002-10-21 Now applies standard' to "unfold" theorem (due to flex-flex constraints).
2002-10-04 paulson 2002-10-04 Fixed bug involving inductive definitions having equalities in the premises, e.g. n = Suc(m).
2002-05-31 berghofe 2002-05-31 Changed interface of MetaSimplifier.rewrite_term.
2002-02-21 wenzelm 2002-02-21 clarified internal theory dependencies;
2002-02-20 wenzelm 2002-02-20 Symbol.bump_string;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-17 wenzelm 2002-01-17 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
2002-01-11 wenzelm 2002-01-11 IsarThy.theorems_i;
2001-12-29 wenzelm 2001-12-29 'inductive_cases': support 'and' form;
2001-12-18 wenzelm 2001-12-18 tuned Type.unify;
2001-12-14 wenzelm 2001-12-14 changed Type.varify;
2001-12-06 wenzelm 2001-12-06 added the_mk_cases;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-21 wenzelm 2001-11-21 Set.vimage;
2001-11-14 wenzelm 2001-11-14 inductive: removed con_defs;
2001-11-13 wenzelm 2001-11-13 tuned;
2001-11-12 wenzelm 2001-11-12 mutual rules declared as ``consumes 0'';
2001-11-09 wenzelm 2001-11-09 tuned;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2001-10-31 wenzelm 2001-10-31 use HOL.induct_XXX;
2001-10-22 wenzelm 2001-10-22 quick_and_dirty_prove_goalw_cterm;
2001-10-18 wenzelm 2001-10-18 GPLed;
2001-10-18 wenzelm 2001-10-18 moved atomize stuff to theory HOL;
2001-10-15 wenzelm 2001-10-15 Tactic.rewrite_cterm;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 "HOL.mono";
2001-10-13 wenzelm 2001-10-13 IsarThy.theorem_i Drule.internalK;
2001-10-04 wenzelm 2001-10-04 simp_case_tac is back again from induct_method.ML; tuned;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-08-16 wenzelm 2001-08-16 prefer immediate monos; tuned;
2001-06-01 paulson 2001-06-01 now checks for leading meta-quantifiers and complains, instead of just raising an exception
2001-02-02 wenzelm 2001-02-02 use hol_simplify;
2001-01-31 wenzelm 2001-01-31 more robust handling of rule cases hints;
2001-01-29 berghofe 2001-01-29 Splitting of arguments of product types in induction rules is now less aggressive.
2001-01-16 wenzelm 2001-01-16 export inductive_forall_name, inductive_forall_def, rulify;
2001-01-06 wenzelm 2001-01-06 Tactic.norm_hhf;
2000-12-27 wenzelm 2000-12-27 Method.erule 0;
2000-12-23 wenzelm 2000-12-23 simplified quick_and_dirty stuff; tuned;
2000-12-22 wenzelm 2000-12-22 handle proper rules;
2000-12-01 wenzelm 2000-12-01 ignore quick_and_dirty for coind;
2000-10-19 wenzelm 2000-10-19 InductAttrib;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-12 nipkow 2000-10-12 induct -> lfp_induct
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-09-23 paulson 2000-09-23 renaming the inverse image operator in HOL