2013-05-30 wenzelm 2013-05-30 more standard fold/fold_rev;
2012-09-12 wenzelm 2012-09-12 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-09-12 wenzelm 2012-09-12 eliminated some old material that is unused in the visible universe;
2012-03-03 wenzelm 2012-03-03 tuned;
2012-01-14 wenzelm 2012-01-14 renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2007-05-31 wenzelm 2007-05-31 tuned headers -- adapted to usual conventions;
2007-05-31 wenzelm 2007-05-31 moved IsaPlanner from Provers to Tools;