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