src/Pure/Isar/expression.ML
2018-03-02 ballarin 2018-03-02 Fall back to reading rewrite morphism first if activation fails without it.
2018-03-02 ballarin 2018-03-02 Proper rewrite morphisms in locale instances.
2018-02-23 wenzelm 2018-02-23 tuned signature;
2018-02-23 wenzelm 2018-02-23 tuned signature;
2018-02-21 wenzelm 2018-02-21 more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
2018-02-21 wenzelm 2018-02-21 minor tuning and clarification;
2018-02-20 wenzelm 2018-02-20 minor tuning and clarification;
2018-02-20 wenzelm 2018-02-20 tuned signature;
2018-02-19 wenzelm 2018-02-19 support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);
2018-02-19 wenzelm 2018-02-19 tuned;
2018-01-16 ballarin 2018-01-16 Experimental support for rewrite morphisms in locale instances.
2017-08-04 haftmann 2017-08-04 provide explicit variant initializers for regular named target vs. almost-named target
2016-07-06 wenzelm 2016-07-06 tuned signature;
2016-07-05 wenzelm 2016-07-05 PIDE reports of implicit variable scope;
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-05-12 wenzelm 2016-05-12 avoid spurious fact index, notably in "context begin" (via Bundle.context);
2016-05-12 wenzelm 2016-05-12 tuned;
2016-05-12 wenzelm 2016-05-12 tuned;
2016-04-12 wenzelm 2016-04-12 Type_Infer.object_logic controls improvement of type inference result;
2016-03-29 wenzelm 2016-03-29 more position information for type mixfix;
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