2015-03-01 wenzelm 2015-03-01 added Proof_Context.cterm_of/ctyp_of convenience;
2015-01-05 haftmann 2015-01-05 formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-08-13 wenzelm 2014-08-13 load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
2014-08-05 wenzelm 2014-08-05 tuned;
2014-06-06 haftmann 2014-06-06 dropped obscure and unused ad-hoc before_exit hook for named targets
2014-05-01 haftmann 2014-05-01 prevent subscription in nested contexts explicitly -- at foundational and user level
2014-04-25 haftmann 2014-04-25 subscription as target-specific implementation device
2014-03-12 wenzelm 2014-03-12 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-02-20 wenzelm 2014-02-20 tuned whitespace;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-30 wenzelm 2013-12-30 tuned whitespace;
2013-12-29 haftmann 2013-12-29 simplified
2013-12-29 haftmann 2013-12-29 more compact representation of different situations for interpretation
2013-12-29 haftmann 2013-12-29 more succint formulation of special case
2013-12-29 haftmann 2013-12-29 tuned whitespace
2013-12-25 haftmann 2013-12-25 ephemeral interpretation also formally works on theory level
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-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-11-23 wenzelm 2013-11-23 more accurate goal context;
2013-08-16 wenzelm 2013-08-16 more markup -- avoid old Locale.extern; removed obsolete Locale.intern -- prefer Locale.check;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-26 haftmann 2013-05-26 more specific structure for registration into theory and dependency onto locale
2013-05-25 wenzelm 2013-05-25 merged
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-05-25 haftmann 2013-05-25 tuned structure
2013-05-22 haftmann 2013-05-22 interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
2013-05-22 haftmann 2013-05-22 mark local theory as brittle also after interpretation inside locales; more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1; check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory
2013-04-24 haftmann 2013-04-24 avoid odd reinit after sublocale declaration
2013-04-23 haftmann 2013-04-23 dropped dead code
2013-04-23 haftmann 2013-04-23 target-sensitive user-level commands interpretation and sublocale
2013-04-23 haftmann 2013-04-23 ML interfaces for various kinds of interpretation
2013-04-23 haftmann 2013-04-23 tuned
2013-04-21 haftmann 2013-04-21 more sharing
2013-04-21 haftmann 2013-04-21 interpretation: distinguish theories and proofs by explicit parameter rather than generic context; formal initialisation of theory target during interpretation; prefer Local_Theory.notes_kind to register mixin equations during interpretation; more uniformity between note_eqns_register and note_eqns_dependency
2013-04-21 haftmann 2013-04-21 dropped unusued identifier
2013-04-21 haftmann 2013-04-21 avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
2013-04-21 haftmann 2013-04-21 tuned for uniformity
2013-03-27 ballarin 2013-03-27 Improvements to the print_dependencies command.
2012-10-11 wenzelm 2012-10-11 refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
2012-10-11 wenzelm 2012-10-11 refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x"; tuned;
2012-10-11 wenzelm 2012-10-11 tuned;
2012-10-11 wenzelm 2012-10-11 tuned;
2012-10-09 wenzelm 2012-10-09 tuned;
2012-04-03 wenzelm 2012-04-03 avoid duplicate PIDE markup; tuned;
2012-04-03 wenzelm 2012-04-03 close context elements via Expression.cert/read_declaration; ensure visible context;
2012-04-03 wenzelm 2012-04-03 tuned;
2012-04-01 wenzelm 2012-04-01 added Attrib.global_notes/local_notes/generic_notes convenience;
2012-03-21 wenzelm 2012-03-21 tuned signature;
2012-03-14 wenzelm 2012-03-14 source positions for locale and class expressions;
2012-03-13 wenzelm 2012-03-13 refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
2012-03-10 wenzelm 2012-03-10 tuned;
2012-03-10 wenzelm 2012-03-10 tuned;
2011-11-19 wenzelm 2011-11-19 simplified Locale.add_thmss, after partial evaluation of attributes;
2011-11-19 wenzelm 2011-11-19 misc tuning;
2011-11-19 wenzelm 2011-11-19 tuned;
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-10-28 wenzelm 2011-10-28 slightly more explicit/syntactic modelling of morphisms;