src/Pure/Isar/expression.ML
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.
2010-06-04 wenzelm 2010-06-04 tuned warning;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-05 haftmann 2010-05-05 eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-15 wenzelm 2010-03-15 replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-19 wenzelm 2010-02-19 Thm.def_binding;
2010-02-18 wenzelm 2010-02-18 locale: more precise treatment of naming vs. binding;
2010-02-16 wenzelm 2010-02-16 comment;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-12 wenzelm 2009-11-12 eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-10-30 haftmann 2009-10-30 tuned variable names of bindings; conceal predicate constants
2009-10-29 wenzelm 2009-10-29 eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-01 ballarin 2009-10-01 Merged.
2009-10-01 ballarin 2009-10-01 Avoid administrative overhead for identity mixins.