2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 ago clarified modules;
2014-03-18 ago tuned signature -- rearranged modules;
2014-03-12 ago tuned signature -- clarified module name;
2014-03-12 ago simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
2014-03-08 ago modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
2014-03-05 ago clarified init_assignable: make double-sure that initial values are reset;
2014-02-28 ago more explicit method reports;
2014-02-26 ago tuned;
2014-02-26 ago method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-16 ago prefer user-space tool within Pure.thy;
2014-02-16 ago more markup;
2014-01-22 ago tuned signature;
2013-12-31 ago proper context for norm_hhf and derived operations;
2013-08-23 ago added Theory.setup convenience;
2013-08-23 ago clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
2013-08-23 ago tuned signature;
2012-08-12 ago tuned;
2012-08-12 ago more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
2012-08-11 ago faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-04-27 ago clarified signature;
2011-11-19 ago added ML antiquotation @{attributes};
2011-10-19 ago proper source positions for @{lemma};
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-04-16 ago modernized structure Proof_Context;
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-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-25 ago modernized naming conventions of main Isar proof elements;
2010-02-07 ago simplified interface for ML antiquotations, struct_name is always "Isabelle";
2009-11-15 ago eliminated obsolete thm position tags;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-03-04 ago ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
2009-01-21 ago removed Ids;
2008-08-14 ago ML_Context.add_antiq: pass position;
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-07-10 ago @{lemma}: allow terminal method, close derivation unless (open) mode is given;
2008-06-28 ago Isar theorem values within ML.