src/HOL/String.thy
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;