author | wenzelm |
Sat, 18 Jan 2014 19:35:42 +0100 | |
changeset 55036 | 87797f8f3152 |
parent 55035 | 68afbb5ce4ff |
child 55037 | 74dfec1edf8c |
--- a/src/HOL/ex/Cartouche_Examples.thy Sat Jan 18 19:31:32 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Sat Jan 18 19:35:42 2014 +0100 @@ -31,7 +31,7 @@ let val c = if Symbol.is_ascii s then ord s - else if s = "" then 10 + else if s = "\<newline>" then 10 else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;