src/Pure/Thy/html.ML

     ("\\<lparr>", (2, "(|")),
     ("\\<rparr>", (2, "|)),")),
     ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
     ("\\<longrightarrow>", (3, "--&gt;")),
     ("\\<rightarrow>", (2, "-&gt;")),
+    ("\\<open>", (1, "&#8249;")),
+    ("\\<close>", (1, "&#8250;")),
     ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
     ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
     ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
     ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];