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.