[isabelle-dev] Default simprules for division in fields
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