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