src/HOL/Euclidean_Division.thy
22 months ago haftmann 2017-10-20 added lemmas and tuned proofs
22 months ago haftmann 2017-10-09 canonical multiplicative euclidean size
22 months ago haftmann 2017-10-09 clarified parity
22 months ago haftmann 2017-10-09 clarified uniqueness criterion for euclidean rings
22 months ago haftmann 2017-10-09 tuned proofs
22 months ago haftmann 2017-10-08 euclidean rings need no normalization
22 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
22 months ago haftmann 2017-10-08 generalized some rules
22 months ago haftmann 2017-10-08 avoid variant of mk_sum
22 months ago haftmann 2017-10-08 generalized simproc
22 months ago haftmann 2017-10-08 elementary definition of division on natural numbers
22 months ago haftmann 2017-10-08 tuned structure
22 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
22 months ago haftmann 2017-10-08 fundamental property of division by units
2017-01-04 haftmann 2017-01-04 moved euclidean ring to HOL