| 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
|
| Thu, 24 Feb 2022 11:25:09 +0000 |
haftmann |
simp rules for negative numerals
|
file |
diff |
annotate
|
| Thu, 17 Feb 2022 19:42:15 +0000 |
haftmann |
more lemmas for distribution
|
file |
diff |
annotate
|
| Thu, 17 Feb 2022 19:42:15 +0000 |
haftmann |
Avoid overaggresive simplification.
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 06:39:36 +0000 |
haftmann |
moved generic implementation into HOL-Main
|
file |
diff |
annotate
|
| Tue, 26 Oct 2021 14:43:59 +0000 |
haftmann |
more generic bit/word lemmas for distribution
|
file |
diff |
annotate
|
| Mon, 11 Oct 2021 06:32:09 +0000 |
haftmann |
more complete simp rules
|
file |
diff |
annotate
|
| Sun, 10 Oct 2021 18:16:57 +0000 |
haftmann |
more complete simp rules
|
file |
diff |
annotate
|
| Sat, 09 Oct 2021 16:41:21 +0000 |
haftmann |
normalizing NOT (numeral _) (again)
|
file |
diff |
annotate
|
| Wed, 29 Sep 2021 06:56:39 +0000 |
haftmann |
repaired slip
|
file |
diff |
annotate
|
| Sat, 25 Sep 2021 07:45:27 +0000 |
haftmann |
NOT is part of syntax bundle also
|
file |
diff |
annotate
|
| Mon, 13 Sep 2021 14:18:24 +0000 |
haftmann |
explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
|
file |
diff |
annotate
|
| Sat, 21 Aug 2021 20:12:15 +0000 |
haftmann |
consolidation of rules for bit operations
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
clarified abstract and concrete boolean algebras
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:53:22 +0000 |
haftmann |
simplified hierarchy of type classes for bit operations
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
| base
|