src/HOL/Tools/inductive.ML
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-12-03 bulwahn 2010-12-03 tuned
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-09-09 haftmann 2010-09-09 only conceal primitive definition theorems, not predicate names
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-23 bulwahn 2010-08-23 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
2010-08-12 haftmann 2010-08-12 Named_Target.theory_init
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-01 bulwahn 2010-08-01 inductive_simps learns to have more tool compliance
2010-07-26 wenzelm 2010-07-26 inductive_cases: crude parallelization via Par_List.map;
2010-07-21 wenzelm 2010-07-21 make SML/NJ happy, by adhoc type-constraints;
2010-07-07 bulwahn 2010-07-07 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-17 wenzelm 2010-05-17 tuned;
2010-05-16 wenzelm 2010-05-16 prefer structure Parse_Spec;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-04 berghofe 2010-05-04 Corrected handling of "for" parameters.
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-04-28 haftmann 2010-04-28 fix "fors" for proof of monotonicity
2010-03-12 bulwahn 2010-03-12 adding Spec_Rules to definitional package inductive and inductive_set
2010-03-08 berghofe 2010-03-08 Added inducts field to inductive_result.
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-31 berghofe 2010-01-31 merged
2010-01-30 berghofe 2010-01-30 Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-30 haftmann 2009-11-30 merged
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-27 berghofe 2009-11-27 Simplified treatment of monotonicity rules.
2009-11-19 wenzelm 2009-11-19 adapted Local_Theory.define -- eliminated odd thm kind;
2009-11-17 wenzelm 2009-11-17 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-10 wenzelm 2009-11-10 merged
2009-11-10 blanchet 2009-11-10 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
2009-11-05 blanchet 2009-11-05 merged
2009-11-05 blanchet 2009-11-05 added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package; this ensures that Nitpick can find the definition and determine whether its inductive or coinductive
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 tuned;
2009-11-05 wenzelm 2009-11-05 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context; tuned signature; tuned;
2009-11-05 wenzelm 2009-11-05 adapted LocalTheory.declaration;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-25 wenzelm 2009-10-25 name space groups are identified by serial, not serial_string;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;