src/HOL/String.thy
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'
2014-02-12 Andreas Lochbihler merged
2014-02-12 Andreas Lochbihler make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
2014-02-12 blanchet adapted theories to 'xxx_case' to 'case_xxx'
2014-01-15 wenzelm added \<newline> symbol, which is used for char/string literals in HOL;
2013-11-20 Andreas Lochbihler setup lifting/transfer for String.literal
2013-10-09 Andreas Lochbihler add congruence rule to prevent code_simp from looping
2013-08-08 Andreas Lochbihler abort execution of generated code with explicit exception message
2013-06-23 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-11 haftmann reflexive nbe equation for equality on String.literal
2013-04-18 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
2013-02-15 haftmann systematic conversions between nat and nibble/char;
2012-10-22 haftmann incorporated constant chars into instantiation proof for enum;
2012-10-20 haftmann moved quite generic material from theory Enum to more appropriate places
2012-10-12 wenzelm discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm prefer ML_file over old uses;
2012-02-15 wenzelm renamed "xstr" to "str_token";
2011-11-14 wenzelm inner syntax positions for string literals;
2011-10-19 bulwahn removing old code generator setup for strings
2011-08-18 haftmann observe distinction between sets and predicates more properly
2011-04-21 wenzelm discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
2011-04-19 wenzelm eliminated Codegen.mode in favour of explicit argument;
2011-03-30 bulwahn renewing specifications in HOL: replacing types by type_synonym
2011-02-10 haftmann reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
2010-09-20 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-13 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-10 bulwahn fiddling with the correct setup for String.literal
2010-09-10 haftmann Haskell == is infix, not infixl
2010-09-09 bulwahn changing String.literal to a type instead of a datatype
2010-09-07 nipkow expand_fun_eq -> ext_iff
2010-08-28 haftmann merged
2010-08-27 haftmann renamed class/constant eq to equal; tuned some instantiations
2010-08-27 wenzelm more antiquotations;
2010-07-08 haftmann tuned module names
2010-04-16 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-02-13 wenzelm modernized structures;
2010-02-11 wenzelm modernized translations;
2010-01-13 haftmann some syntax setup for Scala
2009-10-27 haftmann tuned
2009-10-22 haftmann map_range (and map_index) combinator
2009-07-14 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann code attributes use common underscore convention
2009-06-08 haftmann constant "chars" of all characters
2009-05-19 haftmann String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-17 haftmann is a definition
2009-05-16 bulwahn added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-05-06 haftmann proper structures for list and string code generation stuff
2009-05-06 haftmann refined HOL string theories and corresponding ML fragments
2001-01-15 wenzelm improved string syntax (allow translation rules);
2000-12-23 wenzelm Tools/string_syntax.ML;
1999-08-16 wenzelm 'a list: Nil, Cons;
1999-03-17 wenzelm xstr token class;
1998-07-03 wenzelm moved String theory to main HOL;
less more (0) tip