nipkow at in.tum.de
Sun Feb 15 12:20:47 CET 2015
On 15/02/2015 10:32, Florian Haftmann wrote:
>> 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.
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev