| Thu, 27 Jun 2024 16:52:17 +0000 |
haftmann |
dropped dubious dest rule which always unfolds a definition in the assumptions
|
file |
diff |
annotate
|
| Thu, 09 Nov 2023 15:11:52 +0000 |
haftmann |
slightly less technical formulation of very specific type class
|
file |
diff |
annotate
|
| Thu, 09 Nov 2023 15:11:51 +0000 |
haftmann |
explicit type class for discrete linordered semidoms
|
file |
diff |
annotate
|
| Sat, 16 Sep 2023 06:38:44 +0000 |
haftmann |
reduced prominence of lemma names
|
file |
diff |
annotate
|
| Sat, 16 Sep 2023 06:38:44 +0000 |
haftmann |
new formulation of an auxiliary lemma
|
file |
diff |
annotate
|
| Sat, 01 Oct 2022 07:56:53 +0000 |
haftmann |
reduce prominence of facts
|
file |
diff |
annotate
|
| Thu, 29 Sep 2022 14:03:40 +0000 |
haftmann |
moved relevant theorems from theory Divides to theory Euclidean_Division
|
file |
diff |
annotate
|
| Tue, 13 Sep 2022 12:30:37 +0000 |
haftmann |
more concise instance-specific rules on euclidean relation
|
file |
diff |
annotate
|
| Sun, 11 Sep 2022 16:21:20 +0000 |
haftmann |
dropped auxiliary lemma
|
file |
diff |
annotate
|
| Fri, 09 Sep 2022 21:28:35 +0200 |
haftmann |
less specialized euclidean relation on int
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 16:39:23 +0200 |
haftmann |
clarified generic euclidean relation
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 06:18:23 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 06:18:23 +0000 |
haftmann |
simplified computation algorithm construction
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:17 +0000 |
haftmann |
tuned type signature
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:16 +0000 |
haftmann |
tuned type signature
|
file |
diff |
annotate
|