[isabelle-dev] sign_simps

Larry Paulson lp15 at cam.ac.uk
Sat Feb 14 21:21:35 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. 


> On 14 Feb 2015, at 10:32, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> I see two possibilities:
> * Discontinue sign_simps as an comparingly unfruitful attempt.
> * Turn sign_simps in a proper fact collection like algebra_simps and
> field_simps.  Maybe there are other candidates of splitting rewrite rules?
> Any suggestions on that topic?

More information about the isabelle-dev mailing list