src/Pure/Thy/html.ML
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, "-&gt;")),
     ("\\<open>", (1, "&#8249;")),
     ("\\<close>", (1, "&#8250;")),
+    ("\\<newline>", (1, "&#9166;")),
     ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
     ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
     ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),