2015-11-14 haftmann 2015-11-14 separate ML module for interpretation
2015-10-06 wenzelm 2015-10-06 just one theorem kind, which is legacy anyway;
2015-09-02 wenzelm 2015-09-02 expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;
2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2015-06-14 wenzelm 2015-06-14 improved treatment of Element.Obtains via Expression.prepare_stmt; discontinued pointless all_types ctxt: prep_var is always sequential;
2015-06-14 wenzelm 2015-06-14 clarified context; tuned;
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 wenzelm 2015-03-05 tuned -- more explicit use of context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
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;