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