src/HOL/Tools/string_syntax.ML
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;
less more (0) -10 -2 tip