2012-10-03 ago allow position constraints to coexist with 0 or 1 sort constraints;
2012-10-01 ago report sort assignment of visible type variables;
2012-02-15 ago renamed "xstr" to "str_token";
2012-01-16 ago position constraints for numerals enable PIDE markup;
2011-12-01 ago renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-11-14 ago inner syntax positions for string literals;
2011-11-07 ago discontinued numbered structure indexes (legacy feature);
2011-08-22 ago special treatment of structure index 1 in Pure, including legacy warning;
2011-04-19 ago less bulky "_position", for improved readability of parse trees;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-08 ago discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 ago CONST syntax with positions;
2011-04-08 ago moved CONST syntax/translations to their proper place;
2011-04-08 ago simplified Pure syntax bootstrap;
2011-04-08 ago renamed sprop "prop#" to "prop'" -- proper identifier;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-04-08 ago discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
2011-04-08 ago explicit structure Syntax_Trans;
2011-04-06 ago type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
2011-04-06 ago moved unparse material to syntax_phases.ML;
2011-03-22 ago more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22 ago support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 ago tuned signature of (Context_) variants;
2010-09-01 ago actually declare "_constrainAbs" as @{syntax_const};
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-08 ago renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-04-11 ago Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-27 ago moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
2010-03-22 ago replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 ago minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-03 ago authentic syntax for classes and type constructors;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2010-02-21 ago authentic syntax for *all* term constants;
2010-02-16 ago moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-15 ago renamed InfixName to Infix etc.;
2009-11-15 ago eliminated obsolete thm position tags;
2009-11-08 ago adapted Theory_Data;
2009-11-02 ago modernized structure Simple_Syntax;
2009-10-30 ago set Pure theory name properly
2009-10-25 ago maintain group via name space, not tags;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-09-30 ago eliminated dead code;
2009-07-21 ago join_proofs: implicit exception;
2009-07-19 ago cancel_proofs: some attempts at reworking group management (based on body promises only);
2009-04-02 ago tuned signature;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-03-07 ago Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago Thm.binding;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2009-01-10 ago added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10 ago tuned;
2009-01-10 ago simplified join_proofs;
2008-12-23 ago renamed terminal category "float" to "float_token", to avoid name
2008-12-06 ago renamed force_proofs to join_proofs;
2008-12-05 ago merged
2008-12-04 ago renamed type Lazy.T to lazy;