2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 ago localized default sort;
2010-03-28 ago implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
2010-03-15 ago replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-13 ago added Local_Theory.alias operations (independent of target);
2010-03-01 ago more uniform treatment of syntax for types vs. consts;
2009-11-19 ago Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
2009-11-17 ago uniform new_group/reset_group;
2009-11-13 ago modernized structure Local_Theory;
2009-11-13 ago eliminated slightly odd kind argument of LocalTheory.note(s);
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-05 ago allow "pervasive" local theory declarations, which are applied the background theory;
2009-11-02 ago modernized structure Context_Position;
2009-10-28 ago let naming transform binding beforehand -- covering only the "conceal" flag for now;
2009-10-28 ago added restore_naming;
2009-10-25 ago maintain proper Name_Space.naming, with conceal and set_group;
2009-10-25 ago allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-03-19 ago added map_contexts (cf. Proof.map_contexts);
2009-03-12 ago renamed sticky_prefix to mandatory_path;
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-01-21 ago binding is alias for Binding.T
2008-12-17 ago dropped Ids
2008-12-05 ago dropped NameSpace.declare_base
2008-12-04 ago cleaned up binding module and related code
2008-09-29 ago target update: invisible context position avoids duplication of reports etc.;
2008-09-29 ago added exit_global, exit_result, exit_result_global;
2008-09-27 ago Theory.checkpoint for main operations, admits concurrent proofs;
2008-09-03 ago discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-27 ago type Properties.T;
2008-02-25 ago maintain group in lthy data, implicit use in operations;
2008-01-26 ago grouped versions of axioms/define/notes;
2007-11-10 ago removed LocalTheory.target_naming/name;
2007-11-05 ago simplified LocalTheory.reinit;
2007-10-20 ago tuned abbrev interface;
2007-10-19 ago tuned interfaces;
2007-10-14 ago tuned;
2007-10-13 ago renamed def to define;
2007-10-11 ago local_theory: incorporated consts into axioms;
2007-10-10 ago generalized notation interface (add or del);
2007-10-09 ago removed LocalTheory.defs/target_morphism operations;
2007-09-07 ago fixed type alias in signature;
2007-07-28 ago type Morphism.declaration;
2007-07-28 ago tuned signature;
2007-05-07 ago simplified DataFun interfaces;
2007-02-04 ago added full_naming;
2007-01-28 ago added interface for target_naming;
2006-12-15 ago renamed LocalTheory.assert to affirm;
2006-12-12 ago abbrev: tuned signature;
2006-12-10 ago added notation/abbrev (from term_syntax.ML);
2006-12-07 ago moved notation/abbrevs to TermSyntax;
2006-12-06 ago abbrevs: actually observe target_morphism;
2006-12-05 ago notation/abbreviation: more serious handling of morphisms;
2006-11-30 ago added full_name;
2006-11-26 ago abbrevs: no result;
2006-11-23 ago uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-21 ago LocalTheory.axioms/notes/defs: proper kind;
2006-11-10 ago simplified exit;