src/Pure/Isar/theory_target.ML
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
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-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-21 haftmann 2010-03-21 handle hidden polymorphism in class target (without class target syntax, though)
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-15 wenzelm 2010-03-15 replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-13 wenzelm 2010-03-13 local theory specifications handle hidden polymorphism implicitly;
2010-03-13 wenzelm 2010-03-13 minor tuning and simplification;
2010-03-13 wenzelm 2010-03-13 Local_Defs.contract convenience;
2010-03-11 wenzelm 2010-03-11 more basic Local_Defs.export_cterm;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-18 wenzelm 2010-02-18 removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;
2010-02-15 haftmann 2010-02-15 apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
2009-11-19 wenzelm 2009-11-19 Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
2009-11-17 wenzelm 2009-11-17 uniform new_group/reset_group; tuned signature;
2009-11-15 wenzelm 2009-11-15 eliminated obsolete thm position tags;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-09 wenzelm 2009-11-09 locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-06 wenzelm 2009-11-06 merged
2009-11-04 ballarin 2009-11-04 Merged.
2009-11-02 ballarin 2009-11-02 Relax on type agreement with original context when applying term syntax.
2009-11-05 wenzelm 2009-11-05 allow "pervasive" local theory declarations, which are applied the background theory;
2009-10-28 wenzelm 2009-10-28 misc tuning;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 maintain group via name space, not tags;
2009-09-30 wenzelm 2009-09-30 eliminated redundant parameters;
2009-07-15 wenzelm 2009-07-15 eliminated obsolete legacy_varify;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-06-29 haftmann 2009-06-29 mutual instances
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-13 haftmann 2009-03-13 coherent binding policy with primitive target operations
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
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-11 wenzelm 2009-03-11 more precise treatment of qualified bindings; tuned;
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