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);