src/Pure/conv.ML
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);