| Mon, 09 Oct 2017 19:10:51 +0200 | haftmann | clarified parity | file | diff | annotate |
| Mon, 09 Oct 2017 19:10:49 +0200 | haftmann | clarified uniqueness criterion for euclidean rings | file | diff | annotate |
| Mon, 09 Oct 2017 19:10:48 +0200 | haftmann | tuned proofs | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:22 +0200 | haftmann | euclidean rings need no normalization | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:22 +0200 | haftmann | more fundamental definition of div and mod on int | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:22 +0200 | haftmann | generalized some rules | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:22 +0200 | haftmann | avoid variant of mk_sum | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:21 +0200 | haftmann | generalized simproc | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:21 +0200 | haftmann | elementary definition of division on natural numbers | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:21 +0200 | haftmann | tuned structure | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:21 +0200 | haftmann | abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:19 +0200 | haftmann | fundamental property of division by units | file | diff | annotate |
| Wed, 04 Jan 2017 21:28:29 +0100 | haftmann | moved euclidean ring to HOL | file | diff | annotate |