2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-18 ago more antiquotations;
2014-03-11 ago more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
2014-02-26 ago tuned signature;
2014-02-03 ago more formal markup;
2013-12-31 ago proper context for norm_hhf and derived operations;
2013-12-25 ago self-contained formulation of subclass command, avoiding hard-wired Named_Target.init
2013-12-14 ago proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
2013-09-11 ago tuned signature;
2013-08-23 ago added Theory.setup convenience;
2013-07-30 ago type theory is purely value-oriented;
2013-07-27 ago standardized aliases;
2013-07-13 ago tuned variable names
2013-04-10 ago more standard module name Axclass (according to file name);
2013-03-29 ago convenience check for vain instantiation
2013-03-27 ago tuned signature and module arrangement;
2013-03-25 ago tuned print_classes: more standard order, markup, formatting;
2012-10-03 ago use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
2012-06-17 ago clarifying comment
2012-06-18 ago class target handles additional non-class term parameters appropriately
2012-04-03 ago tuned;
2012-04-03 ago more uniform theory_abbrev with const_declaration;
2012-04-02 ago clarified standard_declaration vs. theory_declaration;
2012-04-01 ago clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
2012-04-01 ago Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
2012-03-22 ago uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
2012-03-22 ago synchronize syntax uniformly for target stack and aux. context;
2012-03-22 ago tuned;
2012-03-21 ago clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-14 ago tuned messages;
2012-03-14 ago more indentation;
2012-03-14 ago eliminated obsolete sanitize_name;
2011-11-09 ago tuned signature;
2011-11-06 ago tuned;
2011-11-05 ago added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
2011-10-30 ago removed obsolete argument (cf. aa35859c8741);
2011-10-28 ago refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
2011-10-28 ago uniform Local_Theory.declaration with explicit params;
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-04-19 ago simplified check/uncheck interfaces: result comparison is hardwired by default;
2011-04-18 ago standardized aliases of operations on tsig;
2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified Sorts.class_error: plain Proof.context;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2010-12-18 ago Add mixins to sublocale command.
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
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-16 ago Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
2010-09-13 ago more precise name for activation of improveable syntax
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-08-26 ago renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
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-20 ago tuned: less formal noise in Named_Target, more coherence in Class
2010-08-12 ago Class.declare -> Class.const
2010-08-11 ago merged