| Sat, 09 Nov 2019 15:39:21 +0000 |
haftmann |
bit shifts as class operations
|
file |
diff |
annotate
|
| Wed, 23 Oct 2019 16:09:23 +0000 |
haftmann |
tuned syntax
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more specialized name for type class
|
file |
diff |
annotate
|
| Sat, 30 Mar 2019 15:37:22 +0100 |
haftmann |
irrelevant
|
file |
diff |
annotate
|
| Thu, 28 Mar 2019 21:24:55 +0100 |
wenzelm |
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
|
file |
diff |
annotate
|
| Fri, 22 Mar 2019 19:18:08 +0000 |
haftmann |
improved code equations taken over from AFP
|
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, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Fri, 20 Apr 2018 07:36:58 +0000 |
haftmann |
algebraic embeddings for bit operations
|
file |
diff |
annotate
|
| Tue, 20 Mar 2018 09:27:39 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 03 Jan 2018 11:06:13 +0100 |
blanchet |
kill old size infrastructure
|
file |
diff |
annotate
|
| Fri, 20 Oct 2017 07:46:10 +0200 |
haftmann |
added lemmas and tuned proofs
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:51 +0200 |
haftmann |
clarified parity
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:49 +0200 |
haftmann |
clarified uniqueness criterion for euclidean rings
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:47 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
euclidean rings need no normalization
|
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
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid fact name clashes
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 09:17:35 +0200 |
haftmann |
more direct construction of integer_of_num;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2017 20:56:38 +0100 |
haftmann |
computation preprocessing rules to allow literals as input for computations
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 18:53:06 +0100 |
haftmann |
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
more fine-grained type class hierarchy for div and mod
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
transfer rules for divides relation on integer and natural
|
file |
diff |
annotate
|
| Wed, 12 Oct 2016 21:48:53 +0200 |
haftmann |
transfer lifting rule for numeral
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:17 +0200 |
haftmann |
do not export abstract constructors in code_reflect
|
file |
diff |
annotate
|