src/Pure/Isar/locale.ML
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
2009-01-07 haftmann 2009-01-07 tuned signature; internal code reorganisation
2009-01-06 haftmann 2009-01-06 merged
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-03 ballarin 2008-12-03 Made global_note_qualified public.
2008-12-01 haftmann 2008-12-01 new Binding module
2008-12-01 haftmann 2008-12-01 Locale.*note* with conventional argument type
2008-12-01 ballarin 2008-12-01 Methods intro_locales and unfold_locales apply to both old and new locales.
2008-11-27 ballarin 2008-11-27 Fixed strange indentation.
2008-11-20 haftmann 2008-11-20 Locale.local_note_qualified
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-17 haftmann 2008-11-17 explicit name morphism function for locale interpretation
2008-11-14 ballarin 2008-11-14 Made local_note_prefix public.
2008-11-14 haftmann 2008-11-14 namify and name_decl combinators
2008-11-13 haftmann 2008-11-13 proper name morphisms for locales
2008-11-10 haftmann 2008-11-10 restruced naming code in anticipation of introduction of name morphisms
2008-11-10 haftmann 2008-11-10 using explicit interpretaton prefix in Name.binding (still on the surface)
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-10-27 ballarin 2008-10-27 Extension of interface: declarations_of.
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-17 ballarin 2008-09-17 Public interface to interpretation morphism.
2008-09-16 ballarin 2008-09-16 Clearer separation of interpretation frontend and backend.
2008-09-03 wenzelm 2008-09-03 Sign.declare_const: Name.binding;
2008-09-03 wenzelm 2008-09-03 Name.qualified;
2008-09-02 ballarin 2008-09-02 Interpretation commands no longer accept interpretation attributes.
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-28 haftmann 2008-08-28 no parameter prefix for class interpretation
2008-08-27 ballarin 2008-08-27 Consistent naming of theorems in interpretation.
2008-08-27 wenzelm 2008-08-27 get rid of tabs;
2008-08-26 ballarin 2008-08-26 Reorganisation of registration code.
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-01 ballarin 2008-08-01 Removed import and lparams from locale record.
2008-07-30 haftmann 2008-07-30 facts_of
2008-07-29 haftmann 2008-07-29 tuned; explicit export of element accessors
2008-07-26 haftmann 2008-07-26 tuned function name
2008-07-25 haftmann 2008-07-25 dropped locale (open)