2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-04-30 ago renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-24 ago curried take/drop
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-27 ago eliminated some old folds;
2009-10-22 ago map_range (and map_index) combinator
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-17 ago explicitly qualify Drule.standard;
2009-10-15 ago replaced String.concat by implode;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-29 ago eliminated hard tabs;
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-01 ago use long names for old-style fold combinators;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2007-09-25 ago Syntax.parse/check/read;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 ago rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-10 ago tuned;
2006-10-20 ago slight cleanup
2006-10-10 ago gen_rem(s) abandoned in favour of remove / subtract
2006-07-25 ago renamed Term.variant_abs to Syntax.variant_abs;
2006-06-19 ago eliminated freeze/varify in favour of Variable.import/export/trade;
2006-06-13 ago tuned;
2006-06-07 ago do not open Logic;
2005-09-12 ago introduced new-style AList operations
2005-07-28 ago Sign.typ_instance;
2005-07-19 ago Logic.incr_tvar;
2005-07-13 ago improved Net interface;
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-05-21 ago Type.typ_instance;
2004-04-22 ago tuned;
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
1999-09-29 ago Sign.defaultS;
1999-07-10 ago handle THM exn;
1998-11-25 ago replaced prs by std_output;
1997-11-21 ago changed Pure/Sequence interface -- isatool fixseq;
1997-07-22 ago Removal of the tactical STATE
1996-11-28 ago Replaced map...~~ by
1996-02-16 ago Elimination of fully-functorial style.
1996-01-29 ago expanded tabs
1994-09-14 ago now uses Sign.const_type;
1994-01-18 ago Updated refs to old Sign functions
1993-09-16 ago Initial revision