2011-11-10 ago tuned signature;
2011-11-09 ago tuned signature;
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-04-19 ago minor tuning and modernization;
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-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-11-28 ago superficial tuning;
2010-09-13 ago more precise name for activation of improveable syntax
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-11 ago tuned internal structure
2010-08-11 ago remove reinit operation alltogether
2010-08-11 ago stripped signature
2010-08-11 ago moved overloading target formally to overloading.ML
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-26 ago eliminanated some unreferenced identifiers;
2010-04-11 ago Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-21 ago tuned whitespace
2010-02-15 ago clarifed type
2009-11-13 ago modernized structure Local_Theory;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-08-15 ago additional checkpoints avoid problems in error situations
2009-07-30 ago improved handling of parameters
2009-07-17 ago tuned/modernized Envir.subst_XXX;
2009-06-17 ago uncheck is liberal wrt. semityped terms
2009-03-13 ago coherent binding policy with primitive target operations
2009-01-21 ago removed Ids;
2009-01-21 ago binding replaces bstring
2008-06-19 ago ProofContext.abbrev_mode;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-22 ago proper abbreviations in class
2008-04-10 ago improvements are strict
2008-04-02 ago tuned
2008-03-12 ago better improvement in instantiation target
2008-03-10 ago tuned
2008-03-07 ago generic improvable syntax for targets
2008-01-08 ago refined overloading target
2007-12-11 ago continued
2007-12-05 ago improved
2007-12-03 ago overloading target