| Mon, 25 Jul 2022 06:31:32 +0000 |
haftmann |
Avoid shadowing original List._ namespace.
|
file |
diff |
annotate
|
| Sat, 09 Jul 2022 08:05:53 +0000 |
haftmann |
refined code equations for characters
|
file |
diff |
annotate
|
| Mon, 04 Jul 2022 07:57:22 +0000 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 09:50:37 +0000 |
haftmann |
Centralized some char-related lemmas in distribution.
|
file |
diff |
annotate
|
| Sat, 02 Apr 2022 17:03:34 +0000 |
haftmann |
tuned whitespace in generated code
|
file |
diff |
annotate
|
| Thu, 17 Feb 2022 19:42:15 +0000 |
haftmann |
Avoid overaggresive simplification.
|
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
|
| 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, 15 Nov 2020 10:13:03 +0000 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
| Wed, 19 Aug 2020 12:58:28 +0100 |
paulson |
Another go with lex: now lexordp back in class ord
|
file |
diff |
annotate
|
| Mon, 17 Aug 2020 15:42:38 +0100 |
paulson |
S Holub's proposed generalisation of the lexicographic product of two orderings
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 18:09:09 +0000 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
| Fri, 08 May 2020 06:26:28 +0000 |
haftmann |
prefer _ mod 2 over of_bool (odd _)
|
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
|
| Sat, 09 Nov 2019 15:39:21 +0000 |
haftmann |
bit shifts as class operations
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more specialized name for type class
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:16:45 +0000 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
file |
diff |
annotate
|
| Fri, 08 Mar 2019 18:56:48 +0000 |
haftmann |
proper code_simp setup for literals
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 22:13:48 +0000 |
haftmann |
prefer proper strings in OCaml
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 11:57:17 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Wed, 25 Apr 2018 09:04:25 +0000 |
haftmann |
uniform tagging for printable and non-printable literals
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 11:52:53 +0000 |
haftmann |
new lemma
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 11:52:52 +0000 |
haftmann |
dedicated append function for string literals
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|