Sun, 15 Nov 2020 10:13:03 +0000 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
Tue, 27 Oct 2020 16:59:44 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Wed, 23 Sep 2020 11:14:38 +0000 |
haftmann |
more thorough treatment of division, particularly signed division on int and word
|
file |
diff |
annotate
|
Thu, 17 Sep 2020 09:57:31 +0000 |
haftmann |
integrated generic conversions into word corpse
|
file |
diff |
annotate
|
Thu, 17 Sep 2020 09:57:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Sat, 05 Sep 2020 08:32:27 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
Sun, 30 Aug 2020 15:15:28 +0000 |
haftmann |
more on conversions
|
file |
diff |
annotate
|
Fri, 21 Aug 2020 18:59:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Sat, 01 Aug 2020 17:43:30 +0000 |
haftmann |
more consequent transferability
|
file |
diff |
annotate
|
Sun, 12 Jul 2020 18:10:06 +0000 |
haftmann |
more simp rules for concrete numerical values
|
file |
diff |
annotate
|
Sat, 11 Jul 2020 18:09:09 +0000 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
Sat, 11 Jul 2020 18:09:08 +0000 |
haftmann |
more thms
|
file |
diff |
annotate
|
Fri, 03 Jul 2020 06:18:29 +0000 |
haftmann |
misc lemma tuning
|
file |
diff |
annotate
|
Sat, 20 Jun 2020 05:56:28 +0000 |
haftmann |
simp rules for conversions
|
file |
diff |
annotate
|
Sat, 20 Jun 2020 05:56:28 +0000 |
haftmann |
more class operations for the sake of efficient generated code
|
file |
diff |
annotate
|
Thu, 18 Jun 2020 09:07:54 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Thu, 21 May 2020 20:00:08 +0000 |
haftmann |
tuned module name space for generated code
|
file |
diff |
annotate
|
Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
Fri, 08 May 2020 06:26:28 +0000 |
haftmann |
prefer _ mod 2 over of_bool (odd _)
|
file |
diff |
annotate
|
Mon, 27 Apr 2020 16:18:51 +0000 |
haftmann |
simplified construction of binary bit operations
|
file |
diff |
annotate
|
Sat, 25 Apr 2020 13:26:24 +0000 |
haftmann |
more rules
|
file |
diff |
annotate
|
Fri, 24 Apr 2020 13:16:41 +0000 |
haftmann |
numeral rules for take_bit / drop_bit on int
|
file |
diff |
annotate
|
Thu, 16 Apr 2020 08:09:31 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
Thu, 16 Apr 2020 08:09:29 +0200 |
haftmann |
bit on numerals
|
file |
diff |
annotate
|
Thu, 16 Apr 2020 08:09:28 +0200 |
haftmann |
more complete rules on numerals
|
file |
diff |
annotate
|
Sun, 08 Mar 2020 17:07:49 +0000 |
haftmann |
more frugal simp rules for bit operations; more pervasive use of bit selector
|
file |
diff |
annotate
|
Tue, 11 Feb 2020 19:03:56 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Sun, 09 Feb 2020 22:03:07 +0000 |
haftmann |
easy abstraction over pointwise bit operations
|
file |
diff |
annotate
|
Sun, 09 Feb 2020 10:46:32 +0000 |
haftmann |
rule concerning bit (push_bit ...)
|
file |
diff |
annotate
|
Sun, 09 Feb 2020 10:21:01 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|