[isabelle-dev] the function "real"
florian.haftmann at informatik.tu-muenchen.de
Sun Nov 15 11:05:15 CET 2015
>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev