2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 ago eliminated aliases of Type.constraint;
2010-08-26 ago 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 ago 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 ago Named_Target.init: empty string represents theory target
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target
2010-08-10 ago Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
2010-08-05 ago Remove duplicate locale activation code; performance improvement.
2010-07-31 ago Interpretation in proofs supports mixins.
2010-07-31 ago Make registrations generic data.
2010-06-04 ago tuned warning;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-05 ago eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-15 ago replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-07 ago modernized structure Object_Logic;
2010-03-07 ago modernized structure Local_Defs;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2010-02-19 ago Thm.def_binding;
2010-02-18 ago locale: more precise treatment of naming vs. binding;
2010-02-16 ago comment;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-13 ago modernized structure Local_Theory;
2009-11-13 ago eliminated slightly odd kind argument of LocalTheory.note(s);
2009-11-12 ago eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-12 ago eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-10 ago modernized structure Theory_Target;
2009-10-30 ago tuned variable names of bindings; conceal predicate constants
2009-10-29 ago eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-28 ago conceal internal bindings;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-01 ago Merged.
2009-10-01 ago Avoid administrative overhead for identity mixins.
2009-10-01 ago merged
2009-10-01 ago Merged.
2009-09-29 ago Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-19 ago Explicit management of registration mixins.
2009-08-19 ago Improved comments and api names.
2009-09-30 ago eliminated redundant parameters;
2009-09-03 ago proper class syntax for sublocale class < expr
2009-07-15 ago simplification of locale interfaces
2009-07-10 ago merged
2009-07-10 ago tuned locale interface
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-03-30 ago prep_full_context_statement: explicit record of flags;
2009-03-29 ago merged
2009-03-29 ago Merged.
2009-03-29 ago Normalise equation only for morphism, not thm stored in theory.
2009-03-29 ago tuned;
2009-03-29 ago simplified Element.activate(_i): singleton version;
2009-03-29 ago tuned;
2009-03-29 ago unified binding prefix terminology;
2009-03-28 ago simplified Locale.activate operations, using generic context;
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
2009-03-28 ago simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-26 ago register_locale: produce stamps at the spot where elements are registered;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);