2012-10-24 ago ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
2011-06-09 ago renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-04-27 ago tuned;
2010-12-17 ago dropped slightly odd Conv.tap_thy
2010-08-23 ago tap_thy conversional
2010-05-15 ago incorporated further conversions and conversionals, after some minor tuning;
2009-10-01 ago moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
2009-02-26 ago Made then_conv and else_conv available as infix operations.
2009-01-21 ago removed Ids;
2008-06-23 ago Logic.is_all;
2008-04-07 ago abs_conv: extra argument for bound variable;
2008-02-25 ago tuned;
2007-10-04 ago abs_conv/forall_conv: proper context (avoid gensym);
2007-07-08 ago gensym: slightly more obscure prefix descreases probability of name clash;
2007-07-05 ago moved type conv to thm.ML;
2007-07-05 ago tuned;
2007-07-05 ago else_conv: only handle THM | CTERM | TERM | TYPE;
2007-07-03 ago removed obsolete goals_conv (cf. prems_conv);
2007-06-25 ago made type conv pervasive;
2007-06-17 ago Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
2007-05-31 ago moved aconvc to more_thm.ML;
2007-05-19 ago added binop_conv, aconvc
2007-05-11 ago unified names: foo_conv;
2007-05-10 ago more conversions;
2007-05-10 ago Conversions: primitive equality reasoning (from drule.ML);