src/HOL/String.thy
6 weeks ago haftmann 2019-03-10 migrated from Nums to Zarith as library for OCaml integer arithmetic
6 weeks ago haftmann 2019-03-08 proper code_simp setup for literals
2 months ago haftmann 2019-01-25 prefer proper strings in OCaml
3 months ago wenzelm 2019-01-06 isabelle update -u path_cartouches;
3 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
5 months ago wenzelm 2018-11-08 isabelle update_cartouches -t;
11 months ago wenzelm 2018-05-20 prefer HTTPS;
12 months ago haftmann 2018-04-25 uniform tagging for printable and non-printable literals
12 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
14 months ago haftmann 2018-02-26 new lemma
14 months ago haftmann 2018-02-26 dedicated append function for string literals
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
17 months ago wenzelm 2017-11-26 more symbols;
20 months ago haftmann 2017-08-03 lifting setup for char
22 months ago haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
22 months ago haftmann 2017-06-24 more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char
2017-02-06 haftmann 2017-02-06 computation preprocessing rules to allow literals as input for computations
2016-12-20 haftmann 2016-12-20 emphasize dedicated rewrite rules for congruences
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-03-19 haftmann 2016-03-19 unified CHAR with CHR syntax
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2016-03-10 haftmann 2016-03-10 moved
2016-02-18 haftmann 2016-02-18 more direct bootstrap of char type, still retaining the nibble representation for syntax
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-07 blanchet 2015-10-07 disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-02-05 haftmann 2015-02-05 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
2015-02-05 haftmann 2015-02-05 explicit type annotation avoids problems with Haskell type inference
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 haftmann 2014-06-30 qualified String.explode and String.implode
2014-06-12 nipkow 2014-06-12 added [simp]
2014-05-04 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-03-07 blanchet 2014-03-07 use balanced tuples in 'primcorec'
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 Andreas Lochbihler 2014-02-12 merged
2014-02-12 Andreas Lochbihler 2014-02-12 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2014-01-15 wenzelm 2014-01-15 added \<newline> symbol, which is used for char/string literals in HOL;
2013-11-20 Andreas Lochbihler 2013-11-20 setup lifting/transfer for String.literal
2013-10-09 Andreas Lochbihler 2013-10-09 add congruence rule to prevent code_simp from looping
2013-08-08 Andreas Lochbihler 2013-08-08 abort execution of generated code with explicit exception message
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-11 haftmann 2013-06-11 reflexive nbe equation for equality on String.literal
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-02-15 haftmann 2013-02-15 systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char
2012-10-22 haftmann 2012-10-22 incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-02-15 wenzelm 2012-02-15 renamed "xstr" to "str_token";
2011-11-14 wenzelm 2011-11-14 inner syntax positions for string literals;