src/HOL/String.thy
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
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-27 wenzelm 2010-08-27 more antiquotations;
2010-07-08 haftmann 2010-07-08 tuned module names
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-02-13 wenzelm 2010-02-13 modernized structures;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2009-10-27 haftmann 2009-10-27 tuned
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-08 haftmann 2009-06-08 constant "chars" of all characters
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-17 haftmann 2009-05-17 is a definition
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-05-06 haftmann 2009-05-06 proper structures for list and string code generation stuff
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2001-01-16 wenzelm 2001-01-16 improved string syntax (allow translation rules);
2000-12-23 wenzelm 2000-12-23 Tools/string_syntax.ML;
1999-08-16 wenzelm 1999-08-16 'a list: Nil, Cons;
1999-03-17 wenzelm 1999-03-17 xstr token class;
1998-07-03 wenzelm 1998-07-03 moved String theory to main HOL;