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