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;
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 ago simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-28 ago minor tuning;
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.);
2009-03-13 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-12 ago renamed NameSpace.bind to NameSpace.define;
2009-03-11 ago eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-01-21 ago wrecked old locale package and related modules
2009-01-17 ago exported depedencies; tuned signature
2009-01-16 ago tuned
2009-01-11 ago explicit bookkeeping of intro rules and axiom