src/HOL/Tools/inductive_set.ML
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-08 wenzelm 2014-08-08 observe context visibility -- less redundant warnings;
2014-04-10 wenzelm 2014-04-10 modernized simproc_setup; modernized theory setup;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-01-01 wenzelm 2014-01-01 clarified simplifier context; eliminated Simplifier.global_context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-01-08 wenzelm 2013-01-08 more tolerant set/pred rule declaration to improve "tool compliance", notably for "context assumes";
2012-09-12 wenzelm 2012-09-12 removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-05 wenzelm 2012-09-05 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2012-03-07 berghofe 2012-03-07 to_pred/set attributes now properly handle variables of type "... => T set"
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-12-24 haftmann 2011-12-24 treatment of type constructor `set`
2011-11-07 wenzelm 2011-11-07 clarified attribute "mono_set": pure declaration, proper export in ML;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for inductive sets in the inductive set package
2011-08-01 nipkow 2011-08-01 infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
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-07-20 wenzelm 2010-07-20 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
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-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-10 haftmann 2010-06-10 moved inductive_codegen to place where product type is available; tuned structure name
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
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-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
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-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-02-25 wenzelm 2010-02-25 more antiquotations;
2010-01-30 berghofe 2010-01-30 Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.
2010-01-14 haftmann 2010-01-14 dropped unused binding
2009-11-19 wenzelm 2009-11-19 adapted Local_Theory.define -- eliminated odd thm kind;
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-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
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-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-08-10 haftmann 2009-08-10 merged
2009-07-30 haftmann 2009-07-30 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-08-04 bulwahn 2009-08-04 removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis