2012-04-27 ago clarified signature;
2012-04-01 ago added Attrib.global_notes/local_notes/generic_notes convenience;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-13 ago suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
2012-03-13 ago improved attribute "abs_def" to handle object-equality as well;
2012-03-03 ago canonical argument order for attribute application;
2012-02-17 ago simplified configuration options for syntax ambiguity;
2012-02-16 ago simplified configuration options for syntax ambiguity;
2012-01-05 ago discontinued Syntax.positions -- atomic parse trees are always annotated;
2011-11-23 ago tuned;
2011-11-21 ago drop vacuous decls;
2011-11-19 ago refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
2011-11-19 ago do not store vacuous theorem specifications -- relevant for frugal local theory content;
2011-11-17 ago partial evaluation in invisible context;
2011-11-16 ago retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
2011-11-16 ago clarified Attrib.partial_evaluation;
2011-11-14 ago some support for partial evaluation of attributed facts;
2011-11-14 ago eliminated dead code;
2011-11-07 ago tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-06 ago more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
2011-08-06 ago make syntax ambiguity warnings a config option
2011-08-08 ago made SML/NJ happy;
2011-08-06 ago extended user-level attribute case_names with names for case hypotheses
2011-06-10 ago tuned name (cf. blast_stats);
2011-05-15 ago optional description for 'attribute_setup' and 'method_setup';
2011-05-14 ago discontinued global config options within attribute name space;
2011-05-03 ago more conventional naming scheme: names_long, names_short, names_unique;
2011-05-02 ago added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
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);