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