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-08-17 ago modernized signature of Term.absfree/absdummy;
2011-06-09 ago discontinued Name.variant to emphasize that this is old-style / indirect;
2010-12-20 ago proper identifiers for consts and types;
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-08-18 ago deglobalization
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-16 ago prefer structure Parse_Spec;
2010-02-28 ago more antiquotations;
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
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-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2008-12-31 ago use regular Term.add_vars, Term.add_frees etc.;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-03-29 ago eliminated quiete_mode ref (not really needed);
2007-10-06 ago simplified interfaces for outer syntax;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-09-25 ago Syntax.parse/check/read;
2007-01-19 ago moved parts of OuterParse to SpecParse;
2006-08-05 ago tuned;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-08 ago Goal.prove_global;
2006-02-07 ago has_duplicates;
2006-02-06 ago subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-01-21 ago simplified type attribute;
2006-01-14 ago generic attributes;
2005-12-09 ago oriented result pairs in PureThy
2005-12-06 ago re-oriented some result tuples in PureThy
2005-10-25 ago avoid legacy goals;
2005-10-21 ago OldGoals;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-08 ago introduces some modern-style AList operations
2005-09-01 ago curried_lookup/update;
2005-08-16 ago OuterKeyword;
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2001-11-15 ago avoid handle _;
2001-11-14 ago fix path prefix;
2001-11-14 ago adapted primrec/datatype to Isar;
2000-07-13 ago adapted PureThy.add_defs_i;
2000-06-28 ago no longer depends upon a prior "open Ind_Syntax" from elsewhere
2000-05-05 ago use Sign.simple_read_term;
2000-03-13 ago adapted to new PureThy.add_thms etc.;
1999-10-21 ago proper handling of axioms / defs;
1999-01-19 ago removal of the (thm list) argument of mk_cases
1999-01-12 ago eliminated tthm type and Attribute structure;
1999-01-06 ago induct_tac and exhaust_tac
1998-12-28 ago new primrec package