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