I really don’t see the gain from getting rid of sign_simps, even if it is
unsuccessful. Except for the occurrence
linordered_field_class.sign_simps(41)
in Multivariate_Analysis/Derivative.thy.
Larry
> On 14 Feb 2015, at 10:32, Florian Haftmann
> <florian.haftm...@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?
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
