2009-07-27 ago moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-03-15 ago simplified method setup;
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-01-21 ago binding replaces bstring
2008-06-25 ago moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-16 ago pervasive RuleInsts;
2008-06-14 ago proper context for tactics derived from res_inst_tac;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-10 ago tuned;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-06 ago simplified interfaces for outer syntax;
2007-10-03 ago avoid unnamed infixes;
2007-09-26 ago Attrib.eval_thms;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-05-07 ago simplified DataFun interfaces;
2007-01-19 ago moved parts of OuterParse to SpecParse;
2006-11-14 ago incorporated IsarThy into IsarCmd;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago generic attributes;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
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-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago refer to name spaces values instead of names;
2005-05-31 ago renamed cond_extern to extern;
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.
2005-01-24 ago Eliminated hack for deleting leading question mark from induction
2003-08-19 ago new case_tac
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-15 ago Isar version of 'rep_datatype';
2001-11-13 ago rearranged inductive package for Isar;
2001-11-08 ago theory data: finish method;
2000-03-13 ago adapted to new PureThy.add_thms etc.;
1999-07-10 ago pass exn;
1999-06-28 ago cond_extern_table;
1999-04-30 ago theory data: copy;
1999-01-19 ago removal of the (thm list) argument of mk_cases
1999-01-13 ago datatype package improvements
1999-01-12 ago eliminated tthm type and Attribute structure;
1999-01-07 ago ZF: the natural numbers as a datatype
1999-01-06 ago induct_tac and exhaust_tac