src/HOL/Tools/inductive_set.ML
2016-07-05 wenzelm 2016-07-05 more antiquotations;
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-25 wenzelm 2016-04-25 clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
2016-04-17 wenzelm 2016-04-17 clarified bindings;
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-12-28 wenzelm 2015-12-28 clarified position information;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-13 wenzelm 2015-09-13 tuned;
2015-09-10 haftmann 2015-09-10 unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification; also unconceal corresponding primitive definitions, which are official conversions between predicates and sets
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-01 wenzelm 2015-06-01 obsolete (see 189c81779a68);
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
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;