| Fri, 18 Apr 2025 14:19:41 +0200 |
haftmann |
explicit check for computations on word type
|
file |
diff |
annotate
|
| Fri, 28 Mar 2025 14:13:40 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 28 Mar 2025 11:56:18 +0100 |
haftmann |
simplified implementation of the_signed_int
|
file |
diff |
annotate
|
| Sun, 12 Jan 2025 21:16:09 +0000 |
paulson |
Simplified a lot of messy proofs
|
file |
diff |
annotate
|
| Mon, 16 Dec 2024 21:08:43 +0100 |
haftmann |
more simp rules on word conversions
|
file |
diff |
annotate
|
| Wed, 09 Oct 2024 23:38:29 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Mon, 26 Aug 2024 21:59:35 +0100 |
paulson |
More tidying of old proofs
|
file |
diff |
annotate
|
| Thu, 20 Jun 2024 14:28:46 +0000 |
haftmann |
dropped references to theorems from transitional theory Divides.thy
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 12:47:51 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2024 16:19:36 +0000 |
haftmann |
simplified specification of type class semiring_bits
|
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
|
| Mon, 29 Jan 2024 20:37:03 +0000 |
haftmann |
strengthened class parity
|
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
|
| Sat, 13 Jan 2024 19:50:15 +0000 |
haftmann |
simplified specification of type class
|
file |
diff |
annotate
|
| Sat, 02 Dec 2023 20:49:50 +0000 |
haftmann |
compactified specification of type class parity
|
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
|
| 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
|
| Tue, 11 Apr 2023 11:59:06 +0000 |
haftmann |
some remarks on division
|
file |
diff |
annotate
|
| Thu, 09 Feb 2023 08:35:50 +0000 |
haftmann |
actually executable enum_all, enum_ex for word
|
file |
diff |
annotate
|
| Tue, 24 Jan 2023 10:30:56 +0000 |
haftmann |
generalized theory name: euclidean division denotes one particular division definition on integers
|
file |
diff |
annotate
|
| Sat, 01 Oct 2022 07:56:53 +0000 |
haftmann |
reduce prominence of facts
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 09:50:40 +0000 |
haftmann |
More lemmas.
|
file |
diff |
annotate
|
| Thu, 17 Feb 2022 19:42:16 +0000 |
haftmann |
Avoid overaggresive splitting.
|
file |
diff |
annotate
|
| Thu, 17 Feb 2022 19:42:15 +0000 |
haftmann |
Avoid overaggresive simplification.
|
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 14:45:53 +0000 |
haftmann |
avoid overaggressive contraction of conversions
|
file |
diff |
annotate
|
| Wed, 29 Sep 2021 06:56:39 +0000 |
haftmann |
repaired slip
|
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
|
| 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
|
| Sun, 01 Aug 2021 10:20:34 +0000 |
haftmann |
organize syntax for word operations in bundles
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Wed, 16 Jun 2021 08:19:09 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 15:49:39 +0000 |
haftmann |
moved more legacy to AFP
|
file |
diff |
annotate
|
| Fri, 28 May 2021 20:21:25 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 28 May 2021 20:21:23 +0000 |
haftmann |
max word moved to Word_Lib in AFP
|
file |
diff |
annotate
|
| Wed, 12 May 2021 17:05:29 +0000 |
haftmann |
explicit type class operations for type-specific implementations
|
file |
diff |
annotate
|
| Tue, 06 Apr 2021 18:12:20 +0000 |
haftmann |
new lemmas
|
file |
diff |
annotate
|
| Sat, 19 Dec 2020 17:49:14 +0000 |
haftmann |
more precise simpset for method unat_arith
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 19:24:36 +0000 |
haftmann |
moved some lemmas from AFP to distribution
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 18:09:02 +0000 |
paulson |
Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 10:13:03 +0000 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 10:03:03 +0000 |
haftmann |
moved most material from session HOL-Word to Word_Lib in the AFP
|
file |
diff |
annotate
| base
|
| Tue, 02 Mar 2010 12:26:50 +0100 |
krauss |
killed more recdefs
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 10:30:36 -0800 |
huffman |
fix more looping simp rules
|
file |
diff |
annotate
|
| Thu, 21 Jan 2010 09:27:57 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:50 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:35:49 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|