src/HOL/String.thy
22 months ago haftmann 2017-08-03 lifting setup for char
24 months ago haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
2017-06-24 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;
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for strings
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-04-21 wenzelm 2011-04-21 discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-03-30 bulwahn 2011-03-30 renewing specifications in HOL: replacing types by type_synonym
2011-02-10 haftmann 2011-02-10 reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-10 bulwahn 2010-09-10 fiddling with the correct setup for String.literal
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-09 bulwahn 2010-09-09 changing String.literal to a type instead of a datatype
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-28 haftmann 2010-08-28 merged