src/Pure/Isar/theory_target.ML
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-05 wenzelm 2009-03-05 Binding.prefix_of;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
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-02-18 haftmann 2009-02-18 fixed signature
2009-02-02 haftmann 2009-02-02 strict check for locale target
2009-01-21 haftmann 2009-01-21 wrecked old locale package and related modules
2009-01-07 haftmann 2009-01-07 tuned siganture of locale.ML
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 rearranged target theories
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-19 ballarin 2008-12-19 All logics ported to new locales.
2008-12-12 ballarin 2008-12-12 Theory target distinguishes old and new locales.
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-13 wenzelm 2008-12-13 removed Ids;
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
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-01 haftmann 2008-12-01 new Binding module
2008-11-20 haftmann 2008-11-20 using name bindings
2008-11-19 ballarin 2008-11-19 Enable switching to new locales during session.
2008-11-18 ballarin 2008-11-18 Code for switching to new locales.
2008-11-17 haftmann 2008-11-17 explicit name morphism function for locale interpretation
2008-11-14 haftmann 2008-11-14 re-educated guess
2008-11-06 haftmann 2008-11-06 cleaned
2008-10-28 ballarin 2008-10-28 Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-27 ballarin 2008-10-27 Hide path in constant name (workaround).
2008-09-22 haftmann 2008-09-22 temporary workaround for class constants
2008-09-03 wenzelm 2008-09-03 discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-02 wenzelm 2008-09-02 tuned;
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-07-29 haftmann 2008-07-29 some steps towards explicit class target for canonical interpretation
2008-06-21 wenzelm 2008-06-21 import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
2008-04-12 wenzelm 2008-04-12 removed unnecessary Goal.close_result;
2008-02-25 wenzelm 2008-02-25 implicit use of LocalTheory.group etc.;
2008-02-10 wenzelm 2008-02-10 tuned spaces;
2008-02-09 wenzelm 2008-02-09 overloading: reduced code redundancy, no xstrings here;
2008-01-26 wenzelm 2008-01-26 grouped versions of axioms/define/notes;
2008-01-24 wenzelm 2008-01-24 replaced ContextPosition by Position.thread_data;
2008-01-08 haftmann 2008-01-08 explicit type variables for instantiation
2007-12-17 haftmann 2007-12-17 note in target
2007-12-11 haftmann 2007-12-11 pretty for instantiation and overloading
2007-12-10 haftmann 2007-12-10 moved instance parameter management from class.ML to axclass.ML
2007-12-05 haftmann 2007-12-05 tuned
2007-12-03 haftmann 2007-12-03 overloading target
2007-11-30 haftmann 2007-11-30 first working version of instance target
2007-11-28 haftmann 2007-11-28 tuned interfaces of class module
2007-11-23 haftmann 2007-11-23 rudimentary instantiation target
2007-11-11 wenzelm 2007-11-11 abbrev: back to PrintMode.internal, which works at least half-way;
2007-11-11 wenzelm 2007-11-11 abbrev: PrintMode.input instead of PrintMode.internal for global version!
2007-11-10 wenzelm 2007-11-10 removed LocalTheory.target_naming/name;
2007-11-10 wenzelm 2007-11-10 locale_const: suppress in class body as well (prevents qualified printing);
2007-11-06 wenzelm 2007-11-06 tuned;
2007-11-06 haftmann 2007-11-06 Class.init now similiar to Locale.init
2007-11-05 wenzelm 2007-11-05 misc cleanup of init functions; renamed init_cmd to context; simplified LocalTheory.reinit;
2007-11-02 haftmann 2007-11-02 clarified theory target interface