Summary
- automatic classical rule to derive a dvd b from b mod a = 0
- consider dvdE for automated classical proving
The file was modified | src/HOL/Rings.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |