| Sat, 02 Dec 2017 16:50:53 +0000 | haftmann | more simplification rules | file | diff | annotate |
| Thu, 23 Nov 2017 17:03:27 +0000 | haftmann | generalized more lemmas | file | diff | annotate |
| Thu, 23 Nov 2017 13:00:00 +0000 | haftmann | new simp rule | file | diff | annotate |
| Sat, 11 Nov 2017 18:41:08 +0000 | haftmann | dedicated definition for coprimality | file | diff | annotate |
| Fri, 20 Oct 2017 07:46:10 +0200 | haftmann | added lemmas and tuned proofs | file | diff | annotate |
| Mon, 09 Oct 2017 19:10:52 +0200 | haftmann | canonical multiplicative euclidean size | file | diff | annotate |
| 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 |