2012-04-27 ago clarified signature;
2012-03-17 ago tuned message;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 ago added ML antiquotation @{keyword};
2011-07-13 ago sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-09 ago simplified Name.variant -- discontinued builtin fold_map;
2011-04-23 ago clarified Type.the_decl;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago more accurate markup for syntax consts, notably binders which point back to the original logical entity;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-01-09 ago reverted 08240feb69c7 -- breaks positions of reports;
2010-12-21 ago more robust ML antiquotations -- allow original tokens without adjacent whitespace;
2010-10-28 ago discontinued obsolete ML antiquotation @{theory_ref};
2010-10-25 ago added ML antiquotation @{assert};
2010-07-21 ago ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
2010-06-03 ago allow qualified names;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-04-16 ago added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-03-09 ago ProofContext.read_class/read_type_name_proper;
2010-03-03 ago authentic syntax for classes and type constructors;
2010-02-27 ago clarified @{const_name} (only logical consts) vs. @{const_abbrev};
2010-02-27 ago ML antiquotations for type classes;
2010-02-25 ago more orthogonal antiquotations for 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 misc tuning and simplification;
2010-02-11 ago added ML antiquotation @{syntax_const};
2010-02-07 ago simplified interface for ML antiquotations, struct_name is always "Isabelle";
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-09-30 ago eliminated redundant bindings;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-25 ago @{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
2009-03-15 ago ML_Syntax.make_binding;
2009-03-13 ago eliminated type Args.T;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-03 ago added @{binding} ML antiquotations;
2009-01-21 ago removed Ids;
2008-08-15 ago Args.name_source(_position) for proper position information;
2008-08-14 ago ML_Context.add_antiq: pass position;
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-06-28 ago moved theorem values to ml_thms.ML;
2008-06-28 ago added macro interface;
2008-06-26 ago Args.context;
2008-06-25 ago re-use official outer keywords;
2008-06-24 ago Common ML antiquotations.