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-05-03 ago minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-04-29 ago proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-27 ago modernized structure Term_Ord;
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_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-21 ago explicitly mark some legacy freeze operations;
2009-11-08 ago adapted Theory_Data;
2009-10-29 ago standardized filter/filter_out;
2009-10-27 ago eliminated some old folds;
2009-10-21 ago merged
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago removed old-style \ and \\ infixes
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-10-17 ago explicitly qualify Drule.standard;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago modernized messages -- eliminated ctyp/cterm operations;
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-07-06 ago structure Thm: less pervasive names;
2009-05-27 ago fixed superficial ML lapses introduced in b3c7044d47b6;
2009-05-25 ago modernized method setup;
2009-03-15 ago simplified attribute setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-12 ago Assumption.all_prems_of, Assumption.all_assms_of;
2009-01-01 ago eliminated OldTerm.(add_)term_consts;
2008-12-31 ago eliminated OldTerm.add_term_free_names;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-29 ago handle _ should be avoided (spurious Interrupt will spoil the game);
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-23 ago Logic.all/mk_equals/mk_implies;
2008-06-12 ago Facts.dest/export_static: content difference;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-16 ago Facts.dest_static;
2008-04-15 ago Facts.dest_table;
2008-03-27 ago eliminated theory ProtoPure;
2008-03-15 ago removed obsolete PureThy.thms_containing_consts;
2007-09-18 ago simplified PrintMode interfaces;
2007-05-10 ago moved some Drule operations to Thm (see more_thm.ML);
2007-05-07 ago simplified DataFun interfaces;
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2006-11-29 ago simplified method setup;
2006-10-20 ago slight cleanup
2006-10-10 ago gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 ago attribute: Context.mapping;
2006-10-04 ago insert replacing ins ins_int ins_string
2006-08-03 ago fixed generator
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-04 ago Thm.varifyT;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2005-11-09 ago Thm.varifyT': natural argument order;
2005-10-21 ago OldGoals;
2005-10-18 ago Simplifier.theory_context;
2005-09-17 ago removed spurious PolyML.exception_trace;