HTML output for \<newline>;
authorwenzelm
Sat, 18 Jan 2014 21:03:54 +0100
changeset 55041 368ee97e03ce
parent 55040 eb3c9b457cb0
child 55042 29e1657b7389
HTML output for \<newline>;
src/Pure/Thy/html.ML
--- 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>")),