2012-04-27 ago clarified signature;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-04-16 ago modernized structure Proof_Context;
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-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-16 ago prefer structure Parse_Spec;
2010-05-12 ago tuned;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-29 ago more explicit treatment of context, although not fully localized;
2010-03-13 ago removed old CVS Ids;
2009-11-08 ago adapted Theory_Data;
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-26 ago simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-13 ago simplified method setup;
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-15 ago Args.name_source(_position) for proper position information;
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2007-10-06 ago simplified interfaces for outer syntax;
2007-09-01 ago replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-05-07 ago simplified DataFun interfaces;
2007-01-19 ago moved parts of OuterParse to SpecParse;
2006-12-18 ago switched argument order in *.syntax lifters
2006-10-09 ago PureThy.note_thmss_i;
2006-08-05 ago tuned;
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-01 ago curried_lookup/update;
2005-08-16 ago OuterKeyword;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-04-13 ago *** empty log message ***
2005-02-13 ago Deleted Library.option type.
2004-07-11 ago local_cla/simpset_of;
2004-06-21 ago Merged in license change from Isabelle2004
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-11 ago IsarThy.theorems_i;
2001-12-29 ago 'inductive_cases': support 'and' form;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-13 ago Generic inductive cases facility for (co)inductive definitions.