2012-04-27 ago clarified signature;
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-15 ago declare minor keywords via theory header;
2012-01-14 ago discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-11-24 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-08-17 ago modernized signature of Term.absfree/absdummy;
2011-08-10 ago old term operations are legacy;
2011-06-29 ago tuned signature;
2011-06-29 ago simplified/unified Simplifier.mk_solver;
2011-06-09 ago renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09 ago discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-01-07 ago do not open ML structures;
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-09-12 ago eliminated aliases of Type.constraint;
2010-08-18 ago deglobalization
2010-07-12 ago moved misc legacy stuff from OldGoals to Misc_Legacy;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-16 ago prefer structure Parse_Spec;
2010-05-05 ago 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 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 ago proper context for rule_by_tactic;
2010-04-29 ago proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29 ago more explicit treatment of context, although not fully localized;
2010-03-27 ago moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-02-28 ago more antiquotations;
2010-02-19 ago moved ancient Drule.get_def to OldGoals.get_def;
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
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-11-02 ago modernized structure Primitive_Defs;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-17 ago explicitly qualify Drule.standard;
2009-09-29 ago modernized Balanced_Tree;
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-03-20 ago Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-19 ago proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 ago more uniform handling of binding in packages;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2009-01-02 ago MetaSimplifier.SIMPLIFIER;
2009-01-01 ago normalized some ML type/val aliases;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-11-18 ago eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
2008-10-23 ago Thm.get_def;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-25 ago tuned;