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-15 ago refer directly to structure Keyword and Parse;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-01 ago tuned signature;
2009-11-01 ago modernized structure Context_Rules;
2009-09-30 ago eliminated redundant bindings;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-15 ago simplified attribute setup;
2009-01-21 ago removed Ids;
2009-01-21 ago binding replaces bstring
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-01-26 ago tuned attribute syntax -- no need for eta-expansion;
2007-06-03 ago tuned Tactic signature;
2007-05-31 ago simplified/unified list fold;
2007-05-07 ago simplified DataFun interfaces;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-26 ago tuned;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-08 ago introduced gen_distinct in place of distinct
2006-02-03 ago canonical member/insert/merge;
2006-01-31 ago tuned;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-15 ago export add_args;
2006-01-13 ago tuned;
2006-01-10 ago generic data and 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-10-28 ago cleaned up nth, nth_update, nth_map and nth_string functions
2005-09-20 ago tuned;
2005-09-20 ago slight adaptions to library changes
2005-09-13 ago tuned;
2005-09-08 ago introduces some modern-style AList operations
2005-06-21 ago tuned;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-05-17 ago tuned;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
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.
2004-06-21 ago Merged in license change from Isabelle2004
2004-03-19 ago Removing the datatype declaration of "order" allows the standard General.order
2002-07-16 ago module now right after ProofContext (for locales);
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
2002-01-17 ago Thm.prop_of;
2001-12-06 ago fixed dest atts;
2001-12-06 ago tuned;
2001-12-05 ago export low-level addXXs;
2001-12-03 ago renamed rule_context.ML to context_rules.ML;