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