| 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
|
| Fri, 19 Aug 2022 05:49:12 +0000 |
haftmann |
streamlined theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:11 +0000 |
haftmann |
more thorough split rules for div and mod on numerals, tuned split rules setup
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:09 +0000 |
haftmann |
consolidated attribute name
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:07 +0000 |
haftmann |
streamlined theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:06 +0000 |
haftmann |
streamlined theorems and sections
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 20:37:16 +0000 |
haftmann |
streamlined primitive definitions for integer division
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Tue, 06 Apr 2021 18:12:20 +0000 |
haftmann |
new lemmas
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 13:08:13 +0000 |
paulson |
trival
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:31 +0000 |
haftmann |
integrated generic conversions into word corpse
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 21 Aug 2020 18:59:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|