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
|