src/Pure/Isar/locale.ML
2010-05-26 ballarin 2010-05-26 Merge mixins of distinct interpretations with same base.
2010-05-24 ballarin 2010-05-24 Store registrations in efficient data structure.
2010-05-24 ballarin 2010-05-24 Avoid recomputation of registration instance for lookup.
2010-05-24 ballarin 2010-05-24 Consistently use equality for registration lookup.
2010-05-24 ballarin 2010-05-24 Cleaner implementation of sublocale command.
2010-05-24 ballarin 2010-05-24 Reapply mixin patch: base for performance improvements.
2010-05-14 ballarin 2010-05-14 Revert mixin patch due to inacceptable performance drop.
2010-05-13 ballarin 2010-05-13 Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
2010-05-04 ballarin 2010-05-04 Merged.
2010-05-04 ballarin 2010-05-04 Provide internal function for printing a single interpretation.
2010-04-27 ballarin 2010-04-27 Explicitly manage export in dependencies.
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-20 ballarin 2010-04-20 Remove garbage.
2010-04-20 ballarin 2010-04-20 Remove garbage.
2010-04-07 ballarin 2010-04-07 Merged resolving conflicts NEWS and locale.ML.
2010-04-02 ballarin 2010-04-02 Proper inheritance of mixins for activated facts and locale dependencies.
2010-02-15 ballarin 2010-02-15 Removed obsolete function.
2010-02-15 ballarin 2010-02-15 Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-02-11 ballarin 2010-02-11 A rough implementation of full mixin inheritance; additional unit tests.
2010-02-02 ballarin 2010-02-02 Clarified invariant; tuned.
2010-02-01 ballarin 2010-02-01 Use serial to be more debug friendly.
2010-03-15 wenzelm 2010-03-15 replaced type_syntax/term_syntax by uniform syntax_declaration;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-09 ballarin 2009-11-09 Removed obsolete code.
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-15 ballarin 2009-10-15 Observe order of declaration when printing registrations.
2009-10-01 ballarin 2009-10-01 Avoid administrative overhead for identity mixins.
2009-09-29 ballarin 2009-09-29 Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-27 ballarin 2009-09-27 Archive registrations by external view.
2009-09-19 ballarin 2009-09-19 Explicit management of registration mixins.
2009-08-19 ballarin 2009-08-19 Improved comments and api names.
2009-07-20 haftmann 2009-07-20 dropped add_registration interface in locale
2009-07-15 haftmann 2009-07-15 simplification of locale interfaces
2009-07-10 haftmann 2009-07-10 tuned locale interface
2009-03-29 wenzelm 2009-03-29 simplified Element.activate(_i): singleton version;
2009-03-29 wenzelm 2009-03-29 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;
2009-03-29 wenzelm 2009-03-29 simplified roundup activation interface;
2009-03-28 wenzelm 2009-03-28 simplified Locale.activate operations, using generic context; misc tuning;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-28 wenzelm 2009-03-28 minor tuning;
2009-03-26 wenzelm 2009-03-26 register_locale: produce stamps at the spot where elements are registered; tuned signature; misc internal tuning and simplification;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-11 wenzelm 2009-03-11 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 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
2009-01-21 haftmann 2009-01-21 wrecked old locale package and related modules
2009-01-17 haftmann 2009-01-17 exported depedencies; tuned signature
2009-01-16 haftmann 2009-01-16 tuned
2009-01-11 haftmann 2009-01-11 explicit bookkeeping of intro rules and axiom