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