src/HOL/Euclidean_Division.thy
23 months ago haftmann 2017-10-08 euclidean rings need no normalization
23 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
23 months ago haftmann 2017-10-08 generalized some rules
23 months ago haftmann 2017-10-08 avoid variant of mk_sum
23 months ago haftmann 2017-10-08 generalized simproc
23 months ago haftmann 2017-10-08 elementary definition of division on natural numbers
23 months ago haftmann 2017-10-08 tuned structure
23 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
23 months ago haftmann 2017-10-08 fundamental property of division by units
2017-01-04 haftmann 2017-01-04 moved euclidean ring to HOL