src/HOL/Tools/inductive_set_package.ML
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-14 haftmann 2008-11-14 Name.is_nothing
2008-11-07 haftmann 2008-11-07 exported codegen_preproc
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-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-05-24 wenzelm 2008-05-24 more uniform treatment of OuterSyntax.local_theory commands;
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-04-03 berghofe 2008-04-03 Added skip_mono flag and inductive_flags type.
2008-03-29 wenzelm 2008-03-29 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
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-02-07 berghofe 2008-02-07 Instead of raising an exception, pred_set_conv now ignores conversion rules that would cause a clash. This allows multiple interpretations of locales containing inductive sets.
2008-01-26 wenzelm 2008-01-26 added theorem group;
2007-11-28 berghofe 2007-11-28 to_set now applies collect_mem_simproc as well.
2007-11-13 berghofe 2007-11-13 to_pred and to_set now save induction and case rule tags.
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs, use plain LocalTheory.def;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-02 wenzelm 2007-10-02 tuned internal interfaces: flags record, added kind for results; tuned;
2007-09-28 berghofe 2007-09-28 add_inductive_i now takes typ instead of typ option as argument.
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-19 berghofe 2007-07-19 strong_ind_simproc now only rewrites arguments of inductive predicates.
2007-07-11 berghofe 2007-07-11 New wrapper for defining inductive sets with new inductive predicate package.