| Mon, 26 Oct 2020 11:28:43 +0000 |
haftmann |
factored out theory Traditional_Syntax
|
file |
diff |
annotate
|
| Sat, 17 Oct 2020 18:56:36 +0200 |
haftmann |
factored out theory Bits_Int
|
file |
diff |
annotate
|
| Thu, 15 Oct 2020 14:55:19 +0200 |
haftmann |
factored out singular operation into separate theory
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sat, 05 Sep 2020 16:21:16 +0000 |
haftmann |
generalized signed_take_bit
|
file |
diff |
annotate
|
| Wed, 05 Aug 2020 19:06:39 +0200 |
haftmann |
separation of reversed bit lists from other material
|
file |
diff |
annotate
|
| Tue, 04 Aug 2020 09:24:00 +0000 |
haftmann |
clearer separation of pre-word bit list material
|
file |
diff |
annotate
|
| Thu, 16 Jul 2020 04:52:25 +0000 |
haftmann |
yet another alias
|
file |
diff |
annotate
|
| Mon, 13 Jul 2020 15:23:32 +0000 |
haftmann |
concatentation of bit values
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 06:21:04 +0000 |
haftmann |
signed_take_bit
|
file |
diff |
annotate
|
| Mon, 06 Jul 2020 10:47:30 +0000 |
haftmann |
separation of traditional bit operations
|
file |
diff |
annotate
|
| Sat, 04 Jul 2020 20:45:24 +0000 |
haftmann |
factored out auxiliary theory
|
file |
diff |
annotate
|
| Fri, 03 Jul 2020 06:18:29 +0000 |
haftmann |
misc lemma tuning
|
file |
diff |
annotate
|
| Thu, 02 Jul 2020 12:10:58 +0000 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| Wed, 01 Jul 2020 17:32:11 +0000 |
haftmann |
factored out ancient numeral representation
|
file |
diff |
annotate
|
| Wed, 01 Jul 2020 17:32:10 +0000 |
haftmann |
more explicit proofs
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:30 +0000 |
haftmann |
build bit operations on word on library theory on bit operations
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
dropped yet another duplicate
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
replaced mere alias by input abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
replaced mere alias by abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
replaced operation with weak abstraction by input abbreviation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
avoid compound operation
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
formal relationships between operations
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
eliminated warnings
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:28 +0000 |
haftmann |
replaced mere alias by input abbreviation
|
file |
diff |
annotate
|
| Sat, 09 May 2020 17:20:04 +0000 |
haftmann |
modernized notation for bit operations
|
file |
diff |
annotate
|
| Thu, 16 Apr 2020 08:09:29 +0200 |
haftmann |
more complete rules on numerals
|
file |
diff |
annotate
|
| Wed, 27 Nov 2019 16:54:33 +0000 |
haftmann |
bit accessor and fundamental properties
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
consolidated map2 clones
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
separate type class for bit comprehension
|
file |
diff |
annotate
|