src/HOL/Tools/inductive_package.ML
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-16 wenzelm 2009-03-16 provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-12 wenzelm 2009-03-12 simplified preparation and outer parsing of specification;
2009-03-11 wenzelm 2009-03-11 explicit Binding.qualified_name -- prevents implicitly qualified bstring;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
2009-03-03 wenzelm 2009-03-03 Binding.str_of;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-25 berghofe 2009-02-25 Use LocalTheory.full_name instead of Sign.full_name, because the latter does not work properly for locales.
2009-02-09 blanchet 2009-02-09 Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.
2009-02-09 blanchet 2009-02-09 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.
2009-02-06 blanchet 2009-02-06 Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-07 wenzelm 2009-01-07 added fork_mono flag, which is usually enabled in batch-mode only; mono rule: unnamed LocalTheory.node ensures proper joining of pending proofs;
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-18 wenzelm 2008-11-18 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac;
2008-11-14 haftmann 2008-11-14 Name.is_nothing
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-09-03 wenzelm 2008-09-03 Name.qualified;
2008-09-02 wenzelm 2008-09-02 made SML/NJ happy;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-18 wenzelm 2008-06-18 OldGoals.read_prop;
2008-05-24 wenzelm 2008-05-24 more uniform treatment of OuterSyntax.local_theory commands;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-22 haftmann 2008-04-22 added explicit check phase after reading of specification
2008-04-03 berghofe 2008-04-03 Added skip_mono flag and inductive_flags type.
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (turned into proper argument);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-25 wenzelm 2008-02-25 inductive package: simplified group handling;
2008-01-26 wenzelm 2008-01-26 added theorem group;
2008-01-03 berghofe 2008-01-03 Added function partition_rules'.
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-10 wenzelm 2007-11-10 put_inductives: be permissive about multiple versions (target names are not necessarily unique); add_inductive: store info under global (!) name -- very rough approximation of the real thing;
2007-11-09 wenzelm 2007-11-09 avoid obsolete Sign.read_prop;
2007-11-05 wenzelm 2007-11-05 improved error message for missing predicates;
2007-10-22 wenzelm 2007-10-22 abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
2007-10-20 wenzelm 2007-10-20 add_inductive: more careful handling of abbrevs -- do not expand prematurely;
2007-10-15 wenzelm 2007-10-15 tuned comment;
2007-10-14 wenzelm 2007-10-14 gen_add_inductive_i: treat abbrevs as local defs, expand by export; tuned;
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs, use plain LocalTheory.def;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-08 haftmann 2007-10-08 integrated FixedPoint into Inductive
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 tuned Induct interface: prefer pred'' over set'';
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-10-02 wenzelm 2007-10-02 tuned internal interfaces: flags record, added kind for results; tuned;