| #
14f1ca5d |
|
28-Jun-2018 |
wenzelm <none@none> |
avoid pending shyps in global theory facts;
|
| #
3e62aabe |
|
02-Dec-2017 |
haftmann <none@none> |
more simplification rules
--HG--
extra : rebase_source : 2b7704ac9459d132ec9fea4769b865bdcad1548f
|
| #
05932626 |
|
23-Nov-2017 |
haftmann <none@none> |
generalized more lemmas
|
| #
ca3200e3 |
|
23-Nov-2017 |
haftmann <none@none> |
new simp rule
|
| #
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality
--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
| #
aab0bfb7 |
|
19-Oct-2017 |
haftmann <none@none> |
added lemmas and tuned proofs
--HG--
extra : rebase_source : 96f42feb3c60e71f2655c97d331ac68baf8b4a63
|
| #
0cca2e53 |
|
09-Oct-2017 |
haftmann <none@none> |
canonical multiplicative euclidean size
--HG--
extra : rebase_source : fad957bbd86aef396df70a1acd8bd096a0a3c82b
|
| #
2c72473b |
|
09-Oct-2017 |
haftmann <none@none> |
clarified parity
--HG--
extra : rebase_source : 7e46e7dfc0f09316c589babeb5a372aeff091071
|
| #
f93a9d94 |
|
09-Oct-2017 |
haftmann <none@none> |
clarified uniqueness criterion for euclidean rings
--HG--
extra : rebase_source : 3f8d28b5e69282e9e5f36f72ad0d4d2e551ca7ab
|
| #
c4bc2aff |
|
09-Oct-2017 |
haftmann <none@none> |
tuned proofs
--HG--
extra : rebase_source : f75a8a3d183658e5e8f4190946b69265b54c84c9
|
| #
fd2471a9 |
|
08-Oct-2017 |
haftmann <none@none> |
euclidean rings need no normalization
--HG--
extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05
|
| #
f740f805 |
|
08-Oct-2017 |
haftmann <none@none> |
more fundamental definition of div and mod on int
--HG--
extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800
|
| #
4ab8e6b4 |
|
08-Oct-2017 |
haftmann <none@none> |
generalized some rules
--HG--
extra : rebase_source : 025e3e1adc961b68e923d241a8e1cb5c2efd0351
|
| #
6641c1a6 |
|
08-Oct-2017 |
haftmann <none@none> |
avoid variant of mk_sum
--HG--
extra : rebase_source : a468f03c9f036febe857eec9455ff61e0e94ddc4
|
| #
5a89ad88 |
|
08-Oct-2017 |
haftmann <none@none> |
generalized simproc
--HG--
extra : rebase_source : 1a484c6a7a8374a73f471204dea8be4ee982845f
|
| #
b01640ea |
|
08-Oct-2017 |
haftmann <none@none> |
elementary definition of division on natural numbers
--HG--
extra : rebase_source : 23767fa1baf28db39b18de60e52d4d7f852e48dd
|
| #
6165cb7f |
|
08-Oct-2017 |
haftmann <none@none> |
tuned structure
--HG--
extra : rebase_source : ad5aac8dba5969d5cd3c3923df071b0e5dad9747
|
| #
2ef94418 |
|
08-Oct-2017 |
haftmann <none@none> |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1
|
| #
cc6c4700 |
|
08-Oct-2017 |
haftmann <none@none> |
fundamental property of division by units
--HG--
extra : rebase_source : ea6719dc07aa4f8e242e1438dc57f98fb74b09cc
|
| #
cc698c8d |
|
04-Jan-2017 |
haftmann <none@none> |
moved euclidean ring to HOL
--HG--
extra : rebase_source : f98dc2e61ffb3cbd04e533f3c0cffa028129e4a2
|