| Thu, 14 Mar 2024 08:24:48 +0000 |
haftmann |
avoid [no_atp] declations shadowing propositions from sledgehammer
|
file |
diff |
annotate
|
| Wed, 21 Feb 2024 16:19:36 +0000 |
haftmann |
simplified specification of type class semiring_bits
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 19:03:14 +0000 |
haftmann |
more on disjunctive addition/subtraction
|
file |
diff |
annotate
|
| Mon, 12 Feb 2024 09:30:22 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 09 Feb 2024 16:43:43 +0000 |
haftmann |
simplified class specification
|
file |
diff |
annotate
|
| Tue, 06 Feb 2024 18:08:43 +0000 |
haftmann |
more lemmas and more correct lemma names
|
file |
diff |
annotate
|
| Mon, 29 Jan 2024 20:37:03 +0000 |
haftmann |
strengthened class parity
|
file |
diff |
annotate
|
| Mon, 29 Jan 2024 19:35:07 +0000 |
haftmann |
common type class for trivial properties on div/mod
|
file |
diff |
annotate
|
| Thu, 25 Jan 2024 11:19:03 +0000 |
haftmann |
rearranged and reformulated abstract classes for bit structures and operations
|
file |
diff |
annotate
|
| Sun, 14 Jan 2024 20:02:58 +0000 |
haftmann |
streamlined type class specification
|
file |
diff |
annotate
|
| Sun, 14 Jan 2024 20:02:55 +0000 |
haftmann |
consolidated lemma name
|
file |
diff |
annotate
|
| Sat, 13 Jan 2024 19:50:15 +0000 |
haftmann |
simplified specification of type class
|
file |
diff |
annotate
|
| Sat, 13 Jan 2024 19:50:12 +0000 |
haftmann |
consolidated name of lemma analogously to nat/int/word_bit_induct
|
file |
diff |
annotate
|
| Sat, 02 Dec 2023 20:49:49 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Sat, 02 Dec 2023 20:49:48 +0000 |
haftmann |
explicit annotation of lemma duplicates
|
file |
diff |
annotate
|
| Tue, 28 Nov 2023 17:39:26 +0000 |
haftmann |
de-duplicated specification of class ring_bit_operations
|
file |
diff |
annotate
|
| Sun, 26 Nov 2023 21:06:47 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Sun, 26 Nov 2023 21:06:46 +0000 |
haftmann |
restructured
|
file |
diff |
annotate
|
| Sun, 26 Nov 2023 21:06:45 +0000 |
haftmann |
grouped lemmas for symbolic computations
|
file |
diff |
annotate
|
| Sun, 26 Nov 2023 21:06:43 +0000 |
haftmann |
sorted out lemma duplicates
|
file |
diff |
annotate
|
| Thu, 23 Nov 2023 16:49:39 +0000 |
haftmann |
slightly more elementary characterization of unset_bit
|
file |
diff |
annotate
|
| Thu, 23 Nov 2023 16:49:39 +0000 |
haftmann |
more direct characterization of binary bit operations
|
file |
diff |
annotate
|
| Wed, 22 Nov 2023 17:50:36 +0000 |
haftmann |
base abstract specification of NOT on recursive equation rather than bit projection
|
file |
diff |
annotate
|
| Tue, 21 Nov 2023 19:19:16 +0000 |
haftmann |
modernized, reordered, generalized
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 15:45:22 +0000 |
haftmann |
operations AND, OR, XOR are specified by characteristic recursive equation
|
file |
diff |
annotate
|
| Sat, 11 Nov 2023 17:44:03 +0000 |
haftmann |
more specific name for type class
|
file |
diff |
annotate
|
| Thu, 09 Nov 2023 15:11:52 +0000 |
haftmann |
slightly less technical formulation of very specific type class
|
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
|
| Mon, 04 Jul 2022 16:12:47 +0000 |
haftmann |
Move code lemmas for symbolic computation of bit operations on int to distribution.
|
file |
diff |
annotate
|