| Sat, 19 Apr 2025 17:39:06 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sun, 16 Mar 2025 14:21:00 +0100 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Mon, 20 Jan 2025 22:15:11 +0100 |
haftmann |
systematic checks for bit operations and more rules on symbolic terms
|
file |
diff |
annotate
|
| Sat, 04 Jan 2025 20:24:12 +0100 |
haftmann |
delegate computation to integer thoroughly
|
file |
diff |
annotate
|
| Sun, 22 Dec 2024 08:46:03 +0100 |
haftmann |
avoid default simp rule which would produce strange recursive unfolding in presence of bit_eq_iff
|
file |
diff |
annotate
|
| Tue, 08 Oct 2024 16:15:31 +0200 |
wenzelm |
more robust declarations via "no syntax" bundles;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2024 23:44:05 +0100 |
paulson |
Some tidying
|
file |
diff |
annotate
|
| 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
|