--- a/src/Pure/Thy/html.ML Fri May 21 21:18:48 2004 +0200
+++ b/src/Pure/Thy/html.ML Fri May 21 21:19:04 2004 +0200
@@ -81,7 +81,6 @@
| "\\<twosuperior>" => (1.0, "²")
| "\\<threesuperior>" => (1.0, "³")
| "\\<acute>" => (1.0, "´")
- | "\\<mu>" => (1.0, "µ")
| "\\<paragraph>" => (1.0, "¶")
| "\\<cdot>" => (1.0, "·")
| "\\<cedilla>" => (1.0, "¸")
@@ -93,7 +92,6 @@
| "\\<threequarters>" => (1.0, "¾")
| "\\<questiondown>" => (1.0, "¿")
| "\\<times>" => (1.0, "×")
- | "\\<emptyset>" => (1.0, "Ø")
| "\\<div>" => (1.0, "÷")
| "\\<circ>" => (1.0, "ˆ")
| "\\<Alpha>" => (1.0, "Α")