[isabelle-dev] Default simprules for division in fields

Lawrence Paulson lp15 at cam.ac.uk
Fri Apr 4 18:12:16 CEST 2014

I wasn’t aware of this detail. But for people who use field_simps explicitly, it neutralises the effect of removing those two as default simprules.


On 4 Apr 2014, at 17:09, Tobias Nipkow <nipkow at in.tum.de> wrote:

> Florian, can you give an example where previously
> field_simps was too weak but with the two additional rules it works?

More information about the isabelle-dev mailing list