>> There are a great many examples of theorems involving various coercion >> functions and the relations =, <, <=. In a number of cases, the “real” >> versions were declared as [iff]-rules, while the “of_nat/of_int” >> versions were declared as [simp]-rules only. When identifying the two, >> I decided it would make sense to go for iff, for maximum automation, >> but I now think this was a mistake. I’m trying the alternative right now. > > Same here. I avoid modifications of the claset as much as possible these > days because it can lead to proof searches going astray although the > goal had nothing to do with those modifications.
I have made similar experiences when trying in vain to turn INF and SUP
into abbreviations.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
