| Thu, 26 Jun 2025 17:25:29 +0200 |
haftmann |
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
|
file |
diff |
annotate
|
| Mon, 21 Apr 2025 08:24:58 +0200 |
haftmann |
more efficient conversions for symbolic representations
|
file |
diff |
annotate
|
| Tue, 15 Apr 2025 19:40:42 +0200 |
haftmann |
corrected operation
|
file |
diff |
annotate
|
| Tue, 15 Apr 2025 19:40:39 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Sat, 05 Apr 2025 08:49:53 +0200 |
haftmann |
incorporate target-language integer implementation of bit shifts into Main
|
file |
diff |
annotate
|
| Thu, 09 Jan 2025 08:33:11 +0100 |
haftmann |
direct symbolic implementations of and, or, xor on integer
|
file |
diff |
annotate
|
| Sat, 04 Jan 2025 20:24:12 +0100 |
haftmann |
delegate computation to integer thoroughly
|
file |
diff |
annotate
|
| Sat, 04 Jan 2025 14:41:30 +0100 |
haftmann |
optionally use shift operations on target numerals for efficient execution
|
file |
diff |
annotate
|
| Sat, 04 Jan 2025 14:25:56 +0100 |
haftmann |
some bit operations on target numerals
|
file |
diff |
annotate
|
| Thu, 02 Jan 2025 08:37:55 +0100 |
haftmann |
refined syntax for code_reserved
|
file |
diff |
annotate
|
| Sat, 28 Dec 2024 21:20:33 +0100 |
nipkow |
Backed out changeset 0ca0a47235e5 (produced Code check failed for Haskell?)
|
file |
diff |
annotate
|
| Mon, 23 Dec 2024 21:58:26 +0100 |
haftmann |
some bit operations on target numerals
|
file |
diff |
annotate
|
| Thu, 19 Dec 2024 15:13:33 +0100 |
haftmann |
more default simp rules
|
file |
diff |
annotate
|
| Fri, 05 Apr 2024 21:21:02 +0200 |
wenzelm |
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2024 16:19:36 +0000 |
haftmann |
simplified specification of type class semiring_bits
|
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 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
|
| Tue, 28 Nov 2023 17:39:26 +0000 |
haftmann |
de-duplicated specification of class ring_bit_operations
|
file |
diff |
annotate
|
| Thu, 23 Nov 2023 16:49:39 +0000 |
haftmann |
slightly more elementary characterization of unset_bit
|
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 |
more correct type annotation
|
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
|