[isabelle-dev] the function "real"

[Florian Haftmann]

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

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