src/HOL/Tools/inductive.ML
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;
2009-10-22 haftmann 2009-10-22 arg_types_of auxiliary function; using multiset operations
2009-10-21 blanchet 2009-10-21 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-21 haftmann 2009-10-21 more accurate removal
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-30 haftmann 2009-09-30 mandatory prefix where appropriate
2009-09-23 haftmann 2009-09-23 stripped legacy ML bindings
2009-09-18 haftmann 2009-09-18 rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
2009-09-18 haftmann 2009-09-18 more antiquotations
2009-07-24 wenzelm 2009-07-24 more antiquotations instead of adhoc ML stuff;
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"