src/HOL/Tools/choice_specification.ML
2012-04-27 ago clarified signature;
2012-03-16 ago eliminated odd 'finalconsts' / Theory.add_finals;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 ago prefer formally checked @{keyword} parser;
2012-03-03 ago canonical argument order for attribute application;
2011-11-19 ago added ML antiquotation @{attributes};
2011-08-10 ago old term operations are legacy;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-26 ago renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-19 ago tuned quotes
2010-08-19 ago use antiquotations for remaining unqualified constants in HOL
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-16 ago prefer structure Parse_Spec;
2010-05-15 ago less pervasive names from structure Thm;
2010-05-04 ago specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result;
2010-05-03 ago renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-03-22 ago eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22 ago replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-17 ago added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-07 ago modernized structure Object_Logic;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-27 ago eliminated some old folds;
2009-10-17 ago explicitly qualify Drule.standard;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"