src/HOL/Tools/string_syntax.ML
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Thu, 25 Feb 2010 22:17:33 +0100 wenzelm explicit @{type_syntax} markup;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:10:01 +0100 wenzelm adapted to authentic syntax;
Sat, 13 Feb 2010 23:24:57 +0100 wenzelm modernized structures;
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Wed, 06 May 2009 16:01:06 +0200 haftmann refined HOL string theories and corresponding ML fragments
Fri, 02 Jan 2009 19:30:12 +0100 wenzelm renamed token markup "_xstr" to "_inner_string";
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Mon, 11 Dec 2006 21:41:05 +0100 wenzelm specials: include single quote;
Sun, 10 Dec 2006 19:37:30 +0100 wenzelm Concrete syntax for hex chars and strings.
Sat, 23 Dec 2000 22:50:19 +0100 wenzelm Tools/string_syntax.ML;
less more (0) tip