--- a/src/Pure/Thy/html.ML Tue Jan 09 23:48:30 2001 +0100
+++ b/src/Pure/Thy/html.ML Wed Jan 10 00:14:52 2001 +0100
@@ -71,6 +71,7 @@
| "\\<yen>" => (1.0, "¥")
| "\\<bar>" => (1.0, "¦")
| "\\<section>" => (1.0, "§")
+ | "\\<dieresis>" => (1.0, "¨")
| "\\<copyright>" => (1.0, "©")
| "\\<ordfeminine>" => (1.0, "ª")
| "\\<guillemotleft>" => (1.0, "«")
@@ -82,9 +83,11 @@
| "\\<plusminus>" => (1.0, "±")
| "\\<twosuperior>" => (1.0, "²")
| "\\<threesuperior>" => (1.0, "³")
+ | "\\<acute>" => (1.0, "´")
| "\\<mu>" => (1.0, "µ")
| "\\<paragraph>" => (1.0, "¶")
| "\\<cdot>" => (1.0, "·")
+ | "\\<cedilla>" => (1.0, "¸")
| "\\<onesuperior>" => (1.0, "¹")
| "\\<ordmasculine>" => (1.0, "º")
| "\\<guillemotright>" => (1.0, "»")
@@ -93,6 +96,7 @@
| "\\<threequarters>" => (1.0, "¾")
| "\\<questiondown>" => (1.0, "¿")
| "\\<times>" => (1.0, "×")
+ | "\\<emptyset>" => (1.0, "Ø")
| "\\<div>" => (1.0, "÷")
| s => (real (size s), implode (map escape (explode s)));