src/HOL/Tools/inductive_realizer.ML
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
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-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-12-13 wenzelm 2011-12-13 'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-08 wenzelm 2011-08-08 added Reconstruct.proof_of convenience;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-01 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 Adapted to new format of proof terms containing explicit proofs of class membership.
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
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-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-30 krauss 2010-03-30 removed dead code; fixed typo
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-17 wenzelm 2009-11-17 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-25 wenzelm 2009-10-25 name space groups are identified by serial, not serial_string;
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-22 wenzelm 2009-07-22 merged, resolving trivial conflict;
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 add_datatypes does not yield particular rules any longer
2009-06-23 haftmann 2009-06-23 add_datatype interface yields type names and less rules
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-16 haftmann 2009-06-16 datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-06-04 haftmann 2009-06-04 avoid Library.foldl_map
2009-05-18 haftmann 2009-05-18 introduced Thm.generatedK
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-15 wenzelm 2009-03-15 simplified attribute setup;
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-07 wenzelm 2009-03-07 more uniform handling of binding in packages;
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-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-07 wenzelm 2009-01-07 inductive: added fork_mono flag;