[isabelle-dev] sign_simps

[Larry Paulson]

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.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?
>