Re: [isabelle] Reversing simp rules



Tobias Nipkow wrote:
> I have implemented a first version with modifier "reorient" and am tempted
> to go with that because it saves you the [symmetric] (after all, the whole
> thing is suppsed to be short, otherwise we wouldn't need it) and does not
> change the behaviour of "add". The word "flip" is a nice too (although a bit
> generic in the context of "auto").

If a short word like "flip" is used, I would suggest to follow the
"simp del:" pattern and use "simp flip:" for the more elaborate methods
(auto, force, etc.), so it's clear that the simp rules are affected.

Cheers,

Bertram




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.