[isabelle-dev] Default simprules for division in fields

[Lawrence Paulson]

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.

Larry

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?