author | wenzelm |
Sat, 18 Jan 2014 21:03:54 +0100 | |
changeset 55041 | 368ee97e03ce |
parent 55040 | eb3c9b457cb0 |
child 55042 | 29e1657b7389 |
--- a/src/Pure/Thy/html.ML Sat Jan 18 20:51:48 2014 +0100 +++ b/src/Pure/Thy/html.ML Sat Jan 18 21:03:54 2014 +0100 @@ -190,6 +190,7 @@ ("\\<rightarrow>", (2, "->")), ("\\<open>", (1, "‹")), ("\\<close>", (1, "›")), + ("\\<newline>", (1, "⏎")), ("\\<^bsub>", (0, hidden "⇘" ^ "<sub>")), ("\\<^esub>", (0, hidden "⇙" ^ "</sub>")), ("\\<^bsup>", (0, hidden "⇗" ^ "<sup>")),