2010-11-28 ago superficial tuning;
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-05 ago turned show_sorts/show_types into proper configuration options;
2010-08-27 ago merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
2010-08-26 ago For sublocale it is sufficient to reconsider ancestors of the target.
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-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 More consistent naming of locale api functions.
2010-07-31 ago print_interps shows interpretations in proofs.
2010-07-31 ago Make registrations generic data.
2010-07-26 ago get_registrations interface
2010-07-21 ago abstract visualization of locale ingredients; all_locales yields proper locale identifiers
2010-06-22 ago Proper treatment of non-inherited mixins.
2010-06-20 ago separate section for diagnostic commands
2010-05-26 ago Merge mixins of distinct interpretations with same base.
2010-05-24 ago Store registrations in efficient data structure.
2010-05-24 ago Avoid recomputation of registration instance for lookup.
2010-05-24 ago Consistently use equality for registration lookup.
2010-05-24 ago Cleaner implementation of sublocale command.
2010-05-24 ago Reapply mixin patch: base for performance improvements.
2010-05-14 ago Revert mixin patch due to inacceptable performance drop.
2010-05-13 ago Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
2010-05-04 ago Merged.
2010-05-04 ago Provide internal function for printing a single interpretation.
2010-04-27 ago Explicitly manage export in dependencies.
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-20 ago Remove garbage.
2010-04-20 ago Remove garbage.
2010-04-07 ago Merged resolving conflicts NEWS and locale.ML.
2010-04-02 ago Proper inheritance of mixins for activated facts and locale dependencies.
2010-02-15 ago Removed obsolete function.
2010-02-15 ago Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-02-11 ago A rough implementation of full mixin inheritance; additional unit tests.
2010-02-02 ago Clarified invariant; tuned.
2010-02-01 ago Use serial to be more debug friendly.
2010-03-15 ago replaced type_syntax/term_syntax by uniform syntax_declaration;
2009-11-12 ago eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-09 ago Removed obsolete code.
2009-11-08 ago adapted Theory_Data;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-10-28 ago conceal internal bindings;
2009-10-25 ago make SML/NJ happy;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-15 ago Observe order of declaration when printing registrations.
2009-10-01 ago Avoid administrative overhead for identity mixins.
2009-09-29 ago Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-27 ago Archive registrations by external view.
2009-09-19 ago Explicit management of registration mixins.
2009-08-19 ago Improved comments and api names.
2009-07-20 ago dropped add_registration interface in locale
2009-07-15 ago simplification of locale interfaces
2009-07-10 ago tuned locale interface
2009-03-29 ago simplified Element.activate(_i): singleton version;
2009-03-29 ago added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
2009-03-29 ago simplified roundup activation interface;
2009-03-28 ago simplified Locale.activate operations, using generic context;