>> So it would be an option to spell out >> simplification rules for »numeral ?x dvd numeral ?y« explicitly using >> type class semiring_numeral_div. > > That sounds like a good solution. It reduces the interdependcies.
See now http://isabelle.in.tum.de/reports/Isabelle/rev/18750e86d5b8 and http://isabelle.in.tum.de/reports/Isabelle/rev/2e19b392d9e3 Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
