changeset 55041 | 368ee97e03ce |
parent 55033 | 8e8243975860 |
child 59448 | 149d2bc5ddb6 |
--- 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>")),