src/HOL/String.thy
Fri, 07 Mar 2014 14:21:15 +0100 blanchet use balanced tuples in 'primcorec'
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
less more (0) -50 -30 tip