src/Pure/Isar/expression.ML
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;
2011-06-25 ballarin 2011-06-25 While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-27 wenzelm 2011-04-27 more uniform Variable.add_frees/add_fixed etc.;
2011-04-21 wenzelm 2011-04-21 discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-16 wenzelm 2011-04-16 tuned signature, disentangled dependencies;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-01-16 wenzelm 2011-01-16 added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-06 ballarin 2011-01-06 Diagnostic command to show locale dependencies.
2010-12-18 ballarin 2010-12-18 Add mixins to sublocale command.
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-08-26 wenzelm 2010-08-26 renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-26 wenzelm 2010-08-26 renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-10 ballarin 2010-08-10 Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
2010-08-05 ballarin 2010-08-05 Remove duplicate locale activation code; performance improvement.
2010-07-31 ballarin 2010-07-31 Interpretation in proofs supports mixins.
2010-07-31 ballarin 2010-07-31 Make registrations generic data.