[isabelle-dev] the function "real"

Florian Haftmann 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
into abbreviations.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151115/7dda1265/attachment.sig>

More information about the isabelle-dev mailing list