| Thu, 31 Oct 2019 09:02:02 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Wed, 23 Oct 2019 16:09:23 +0000 |
haftmann |
tuned syntax
|
file |
diff |
annotate
|
| Tue, 22 Oct 2019 19:07:11 +0000 |
haftmann |
bit operations for word type
|
file |
diff |
annotate
|
| Sat, 19 Oct 2019 09:15:41 +0000 |
haftmann |
added quickcheck setup
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
more theorems for proof of concept for word type
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:07 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 05 Apr 2018 06:15:02 +0000 |
haftmann |
even more on bit operations
|
file |
diff |
annotate
|
| Wed, 21 Mar 2018 19:39:23 +0100 |
haftmann |
prefer convention to place operation name before type name
|
file |
diff |
annotate
|
| Sat, 10 Mar 2018 19:36:59 +0000 |
haftmann |
abstract algebraic bit operations
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
one uniform type class for parity structures
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| Sat, 08 Oct 2016 14:09:55 +0200 |
haftmann |
tuned name of bit truncating operations
|
file |
diff |
annotate
|
| Sat, 08 Oct 2016 14:09:53 +0200 |
haftmann |
dedicated syntax for types with a length
|
file |
diff |
annotate
|
| Mon, 03 Oct 2016 14:37:06 +0200 |
haftmann |
proof of concept for algebraically founded word types
|
file |
diff |
annotate
|