2011-04-17 ago markup attributes/methods via name space;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 ago discontinued special status of structure Printer;
2011-04-08 ago explicit structure Syntax_Trans;
2011-04-07 ago tuned signature;
2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-03-22 ago enable inner syntax source positions by default (controlled via configuration option);
2010-12-21 ago configuration option "syntax_ast_trace" and "syntax_ast_stat";
2010-12-21 ago configuration option "ML_trace";
2010-12-17 ago renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-16 ago turned simp_trace_depth_limit into a configuration option
2010-12-02 ago configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02 ago renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-10-30 ago support for real valued configuration options;
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-17 ago tuned signature of (Context_) variants;
2010-09-06 ago turned show_hyps and show_tags into proper configuration option;
2010-09-06 ago more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-05 ago turned show_brackets into proper configuration option;
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-03 ago turned eta_contract into proper configuration option;
2010-09-03 ago turned show_structs into proper configuration option;
2010-09-03 ago configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
2010-09-03 ago pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-03 ago treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
2010-09-03 ago more explicit Config.declare vs. Config.declare_global;
2010-09-03 ago turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
2010-09-03 ago turned show_consts into proper configuration option;
2010-09-02 ago turned show_question_marks into proper configuration option;
2010-08-11 ago tuned eval_thms (cf. note etc. in proof.ML);
2010-08-11 ago use Pretty.enum convenience;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-10 ago renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 ago pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
2010-03-28 ago configuration options admit dynamic default values;
2010-03-28 ago do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
2010-03-26 ago replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-07 ago modernized structure Object_Logic;
2010-03-07 ago modernized structure Local_Defs;
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;
2010-01-30 ago Added "constraints" tag / attribute for specifying the number of equality
2009-11-13 ago eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-08 ago adapted Theory_Data;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-25 ago make SML/NJ happy;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-02 ago merged, resolving conflict in src/Pure/Isar/attrib.ML;
2009-06-02 ago made SML/NJ happy
2009-06-01 ago made SML/NJ happy;
2009-05-30 ago eliminated old Attrib.add_attributes (and Attrib.syntax);
2009-05-30 ago modernized attribute setup;
2009-05-18 ago introduced Thm.generatedK
2009-05-16 ago added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages