2016-06-22 ago report class parameters within instantiation;
2016-04-09 ago removed old proof method "default";
2016-03-30 ago tuned messages -- position is usually missing here;
2016-03-29 ago more position information for type mixfix;
2015-12-19 ago abandoned attempt to unify sublocale and interpretation into global theories
2015-09-25 ago tuned signature: eliminated pointless type Context.pretty;
2015-09-02 ago trim context for persistent storage;
2015-07-28 ago clarified context;
2015-06-30 ago no arguments for "standard" (or old "default") methods;
2015-06-30 ago renamed "default" to "standard", to make semantically clear what it is;
2015-06-01 ago explicit argument expansion of uncheck rules;
2015-06-01 ago explicit input marker for operations
2015-06-01 ago completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
2015-06-01 ago self-contained formulation of abbrev for named targets
2015-06-01 ago clearly separated target primitives (target_foo) from self-contained target operations (foo)
2015-06-01 ago clarified interfaces for improvable syntax
2015-06-01 ago tuned
2015-05-03 ago tuned output to resemble input syntax more closely;
2015-05-03 ago tuned output;
2015-04-02 ago sort constraints are inherent part of class abbreviations (in contrast to class constants)
2015-03-31 ago tuned;
2015-02-10 ago proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2015-01-22 ago backed out obsolete workaround from ef1edfb36af7
2015-01-21 ago option for formally inlined class specifications in hierarchy graph
2015-01-17 ago more compact content for tighter graph layout;
2015-01-17 ago clarified Class.pretty_specification: imitate input source;
2015-01-05 ago formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
2014-12-19 ago tuned;
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-30 ago eliminated aliases;
2014-10-13 ago tuned signature;
2014-06-08 ago yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
2014-06-08 ago re-unified approach towards class and locale consts, with refined terminology: foo_const_declaration denotes declaration for a particular logical layer, foo_const the full stack for a particular target
2014-06-08 ago revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
2014-06-08 ago less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only;
2014-06-07 ago treat non-canonical interpretations of classes the same way as ordinary locale interpretations
2014-06-05 ago always refine interpretation morphism using canonical constant's definition theorem
2014-06-02 ago formal treatment of dangling parameters for class abbrevs analogously to class consts
2014-06-01 ago definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
2014-06-01 ago tuned
2014-05-31 ago postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
2014-05-31 ago tuned
2014-05-31 ago explicit is better than implicit
2014-05-31 ago tuned names
2014-05-31 ago dropped accidental duplicate application of morphism
2014-05-30 ago tuned
2014-05-28 ago tuned variable names
2014-05-22 ago tuned names
2014-05-22 ago moved const declaration further down in bootstrap hierarchy: keep Named_Target free of low-level stuff
2014-05-22 ago tuned
2014-05-22 ago more uniform order of operations;
2014-05-22 ago tuned signature
2014-04-25 ago subscription as target-specific implementation device
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