2022-07-25 |
haftmann |
Avoid shadowing original List._ namespace.
|
file |
diff |
annotate
|
2022-07-09 |
haftmann |
refined code equations for characters
|
file |
diff |
annotate
|
2022-07-04 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
2022-06-25 |
haftmann |
Centralized some char-related lemmas in distribution.
|
file |
diff |
annotate
|
2022-04-02 |
haftmann |
tuned whitespace in generated code
|
file |
diff |
annotate
|
2022-02-17 |
haftmann |
Avoid overaggresive simplification.
|
file |
diff |
annotate
|
2021-09-13 |
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
|
2021-08-03 |
haftmann |
simplified hierarchy of type classes for bit operations
|
file |
diff |
annotate
|
2021-08-02 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
2020-11-15 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
2020-08-19 |
paulson |
Another go with lex: now lexordp back in class ord
|
file |
diff |
annotate
|
2020-08-17 |
paulson |
S Holub's proposed generalisation of the lexicographic product of two orderings
|
file |
diff |
annotate
|
2020-07-11 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
2020-05-08 |
haftmann |
prefer _ mod 2 over of_bool (odd _)
|
file |
diff |
annotate
|
2020-03-08 |
haftmann |
more frugal simp rules for bit operations; more pervasive use of bit selector
|
file |
diff |
annotate
|
2019-11-09 |
haftmann |
bit shifts as class operations
|
file |
diff |
annotate
|
2019-06-14 |
haftmann |
slightly more specialized name for type class
|
file |
diff |
annotate
|
2019-03-10 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
file |
diff |
annotate
|
2019-03-08 |
haftmann |
proper code_simp setup for literals
|
file |
diff |
annotate
|
2019-01-25 |
haftmann |
prefer proper strings in OCaml
|
file |
diff |
annotate
|
2019-01-06 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
2018-11-08 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
2018-05-20 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
2018-04-25 |
haftmann |
uniform tagging for printable and non-printable literals
|
file |
diff |
annotate
|
2018-04-24 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
2018-02-26 |
haftmann |
new lemma
|
file |
diff |
annotate
|
2018-02-26 |
haftmann |
dedicated append function for string literals
|
file |
diff |
annotate
|
2018-01-10 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2017-08-03 |
haftmann |
lifting setup for char
|
file |
diff |
annotate
|
2017-07-02 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
2017-06-24 |
haftmann |
more direct construction of integer_of_num;
|
file |
diff |
annotate
|
2017-02-06 |
haftmann |
computation preprocessing rules to allow literals as input for computations
|
file |
diff |
annotate
|
2016-12-20 |
haftmann |
emphasize dedicated rewrite rules for congruences
|
file |
diff |
annotate
|
2016-09-26 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
2016-03-19 |
haftmann |
unified CHAR with CHR syntax
|
file |
diff |
annotate
|
2016-03-12 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
2016-03-10 |
haftmann |
moved
|
file |
diff |
annotate
|
2016-02-18 |
haftmann |
more direct bootstrap of char type, still retaining the nibble representation for syntax
|
file |
diff |
annotate
|
2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
2015-10-07 |
blanchet |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
file |
diff |
annotate
|
2015-09-01 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
2015-08-27 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
2015-07-27 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
2015-03-06 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
2015-03-06 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
2015-02-05 |
haftmann |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
file |
diff |
annotate
|
2015-02-05 |
haftmann |
explicit type annotation avoids problems with Haskell type inference
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
2014-10-29 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
2014-09-11 |
blanchet |
updated news
|
file |
diff |
annotate
|
2014-09-02 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
2014-06-30 |
haftmann |
qualified String.explode and String.implode
|
file |
diff |
annotate
|
2014-06-12 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
2014-05-04 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
2014-03-07 |
blanchet |
use balanced tuples in 'primcorec'
|
file |
diff |
annotate
|
2014-02-20 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|