| 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
|
| 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
|
| 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
|