src/Pure/Isar/class.ML
2015-05-03 wenzelm 2015-05-03 tuned output to resemble input syntax more closely;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-04-02 haftmann 2015-04-02 sort constraints are inherent part of class abbreviations (in contrast to class constants)
2015-03-31 wenzelm 2015-03-31 tuned;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-22 haftmann 2015-01-22 backed out obsolete workaround from ef1edfb36af7
2015-01-21 haftmann 2015-01-21 option for formally inlined class specifications in hierarchy graph
2015-01-17 wenzelm 2015-01-17 more compact content for tighter graph layout;
2015-01-17 wenzelm 2015-01-17 clarified Class.pretty_specification: imitate input source;
2015-01-05 haftmann 2015-01-05 formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
2014-12-19 wenzelm 2014-12-19 tuned;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-13 wenzelm 2014-10-13 tuned signature;
2014-06-08 haftmann 2014-06-08 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 haftmann 2014-06-08 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 haftmann 2014-06-08 revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
2014-06-08 haftmann 2014-06-08 less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only; n.b. this fullfills promise given in 63c7b29d29ac
2014-06-07 haftmann 2014-06-07 treat non-canonical interpretations of classes the same way as ordinary locale interpretations
2014-06-05 haftmann 2014-06-05 always refine interpretation morphism using canonical constant's definition theorem
2014-06-02 haftmann 2014-06-02 formal treatment of dangling parameters for class abbrevs analogously to class consts
2014-06-01 haftmann 2014-06-01 definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
2014-06-01 haftmann 2014-06-01 tuned
2014-05-31 haftmann 2014-05-31 postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
2014-05-31 haftmann 2014-05-31 tuned
2014-05-31 haftmann 2014-05-31 explicit is better than implicit
2014-05-31 haftmann 2014-05-31 tuned names
2014-05-31 haftmann 2014-05-31 dropped accidental duplicate application of morphism
2014-05-30 haftmann 2014-05-30 tuned
2014-05-28 haftmann 2014-05-28 tuned variable names
2014-05-22 haftmann 2014-05-22 tuned names
2014-05-22 haftmann 2014-05-22 moved const declaration further down in bootstrap hierarchy: keep Named_Target free of low-level stuff
2014-05-22 haftmann 2014-05-22 tuned
2014-05-22 haftmann 2014-05-22 more uniform order of operations; tuned names
2014-05-22 haftmann 2014-05-22 tuned signature
2014-04-25 haftmann 2014-04-25 subscription as target-specific implementation device
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-18 wenzelm 2014-03-18 more antiquotations;
2014-03-11 wenzelm 2014-03-11 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 wenzelm 2014-02-26 tuned signature;
2014-02-03 wenzelm 2014-02-03 more formal markup;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-25 haftmann 2013-12-25 self-contained formulation of subclass command, avoiding hard-wired Named_Target.init
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-09-11 wenzelm 2013-09-11 tuned signature;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-07-13 haftmann 2013-07-13 tuned variable names
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-03-29 haftmann 2013-03-29 convenience check for vain instantiation
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-25 wenzelm 2013-03-25 tuned print_classes: more standard order, markup, formatting; uniform printing of minimal supersort/classrel;
2012-10-03 wenzelm 2012-10-03 use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
2012-06-17 haftmann 2012-06-17 clarifying comment
2012-06-18 haftmann 2012-06-18 class target handles additional non-class term parameters appropriately
2012-04-03 wenzelm 2012-04-03 tuned;
2012-04-03 wenzelm 2012-04-03 more uniform theory_abbrev with const_declaration;
2012-04-02 wenzelm 2012-04-02 clarified standard_declaration vs. theory_declaration;
2012-04-01 wenzelm 2012-04-01 clarified Generic_Target.notes: always perform Attrib.partial_evaluation; more uniform Generic_Target.theory_notes/locale_notes: apply facts to all target contexts;