src/Tools/IsaPlanner/rw_inst.ML
2015-06-02 wenzelm 2015-06-02 clarified context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-09-11 blanchet 2014-09-11 fixed some spelling mistakes
2013-05-30 wenzelm 2013-05-30 tuned signature; tuned;
2013-05-30 wenzelm 2013-05-30 more standard fold/fold_rev;
2013-05-30 wenzelm 2013-05-30 misc tuning;
2013-05-30 wenzelm 2013-05-30 prefer existing beta_eta_conversion;
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;
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-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
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-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
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;
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;