src/HOL/Tools/string_syntax.ML
Mon, 30 Sep 2024 20:30:59 +0200 wenzelm clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
Sun, 01 Sep 2024 19:35:30 +0200 wenzelm proper string syntax (amending 70076ba563d2);
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sat, 08 Sep 2018 08:09:07 +0000 haftmann more explicit notion of ord value for HOL characters
Sun, 06 May 2018 18:20:25 +0000 haftmann typo
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Sat, 12 Mar 2016 22:04:52 +0100 haftmann model characters directly as range 0..255
Wed, 29 Oct 2014 15:07:53 +0100 wenzelm modernized setup;
Wed, 22 Jan 2014 15:10:33 +0100 wenzelm inner syntax token language allows regular quoted strings;
Wed, 15 Jan 2014 23:25:28 +0100 wenzelm added \<newline> symbol, which is used for char/string literals in HOL;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Fri, 15 Feb 2013 11:47:33 +0100 haftmann systematic conversions between nat and nibble/char;
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;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
less more (0) -15 tip