2007-07-29 ago moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-05 ago added is_reflexive;
2007-06-25 ago added reasonably efficient add_cterm_frees;
2007-05-31 ago made aconvc pervasive;
2007-05-31 ago moved aconvc to more_thm.ML;
2007-05-10 ago added destructors from drule.ML;
2007-04-15 ago moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-14 ago added read_def_cterms, read_cterm (from thm.ML);
2007-02-28 ago tuned;
2007-02-26 ago Further operations on type thm, outside the inference kernel.