| Sun, 09 Feb 2020 10:46:32 +0000 |
haftmann |
rule concerning bit (push_bit ...)
|
file |
diff |
annotate
|
| Sat, 01 Feb 2020 19:10:40 +0100 |
haftmann |
more specific class assumptions
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 17:15:16 +0000 |
haftmann |
tuned material
|
file |
diff |
annotate
|
| Sun, 01 Dec 2019 08:00:59 +0000 |
haftmann |
characterization of singleton bit operation
|
file |
diff |
annotate
|
| Sun, 17 Nov 2019 20:44:35 +0000 |
haftmann |
strengthened type class for bit operations
|
file |
diff |
annotate
|
| 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
|
| Fri, 18 Dec 2015 14:23:11 +0100 |
Andreas Lochbihler |
add serialisation for abs on integer to target language operation
|
file |
diff |
annotate
|
| Sun, 27 Sep 2015 10:11:15 +0200 |
haftmann |
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
|
file |
diff |
annotate
|
| Sun, 27 Sep 2015 10:11:14 +0200 |
haftmann |
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 08 Aug 2015 10:51:33 +0200 |
haftmann |
direct bootstrap of integer division from natural division
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2015 16:55:28 +0100 |
paulson |
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
distributivity of partial minus establishes desired properties of dvd in semirings
|
file |
diff |
annotate
|
| Fri, 06 Feb 2015 17:57:03 +0100 |
haftmann |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 18:48:54 +0200 |
haftmann |
always annotate potentially polymorphic Haskell numerals
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
keep obsolete interpretations in Main, to avoid merge trouble
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:57:10 +0200 |
blanchet |
reintroduced an instantiation of 'size' for 'numerals'
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved old 'size' generator together with 'old_datatype'
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 19:07:14 +0100 |
kuncar |
unregister lifting setup following the best practice of Lifting
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 10:59:25 +0100 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 09:06:04 +0100 |
Andreas Lochbihler |
make integer_of_char and char_of_integer work with NBE and code_simp
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|