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 <[email protected]> wrote: > Florian, can you give an example where previously > field_simps was too weak but with the two additional rules it works? _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
