florian.haftmann at informatik.tu-muenchen.de
Sun Feb 15 15:25:56 CET 2015
>>> I really don’t see the gain from getting rid of sign_simps, even if
>>> it is unsuccessful. Except for the occurrence
>>> in Multivariate_Analysis/Derivative.thy.
>> My primary concern is actually the comment which states that some rules
>> have not been added to field_simps since the lead to splitting. So the
>> question is whether it would make sense to identify more sensible but
>> splitting rewrite rules and establish a fact collection which contains
>> field_simps but also those splitting rules. Especially fields with case
>> distinctions (!)= 0 could bear likely candidates.
> I have been using field_simps a lot lately and was happy with it. I
> would not want to modify it without concrete practical shortcomings.
I do not suggest to modify field_simps, but ask myself whether a
further, broader fact collection would make sender.
Anyway, this has no high priority and seems to require further
iterations of thinking.
>> The broader context is that I have made an investigation for theorems
>> which are equivalent except in their sort constraints. These are likely
>> to exhibit irregularities in the class hierarchy.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev