Skip to content
Success

Changes

Summary

  1. automatic classical rule to derive a dvd b from b mod a = 0
  2. consider dvdE for automated classical proving
Changeset 68252:8b284d24f434 by haftmann:
automatic classical rule to derive a dvd b from b mod a = 0
The file was modified src/HOL/Rings.thy (diff)
Changeset 68251:54a127873735 by haftmann:
consider dvdE for automated classical proving
The file was modified src/HOL/Rings.thy (diff)