2011-11-14 ago pass positions for named targets, for formal links in the document model;
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-11-05 ago tuned;
2011-11-05 ago misc tuning;
2011-10-30 ago even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);
2011-10-30 ago removed obsolete argument (cf. aa35859c8741);
2011-10-29 ago uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
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-10-28 ago tuned signature -- refined terminology;
2011-04-16 ago modernized structure Proof_Context;
2011-03-13 ago tuned headers;
2011-01-16 ago added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2010-11-28 ago superficial tuning;
2010-09-22 ago tuned
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-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-20 ago tuned: less formal noise in Named_Target, more coherence in Class
2010-08-12 ago Class.declare -> Class.const
2010-08-12 ago named target is optional; explicit Name_Target.reinit
2010-08-12 ago Named_Target.init: empty string represents theory target
2010-08-12 ago Named_Target.theory_init
2010-08-11 ago remove reinit operation alltogether
2010-08-11 ago more convenient split of class modules: class and class_declaration
2010-08-11 ago tuned
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target