src/HOL/Divides.thy
1999-07-19 paulson 1999-07-19 new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
1999-07-01 paulson 1999-07-01 now div and mod are overloaded; dvd is polymorphic
1997-05-30 paulson 1997-05-30 Moving div and mod from Arith to Divides Moving dvd from ex/Primes to Divides