output_tym: removed duplicate clauses;
authorwenzelm
Fri, 21 May 2004 21:19:04 +0200
changeset 14775 65c22319829f
parent 14774 d747c32e85e1
child 14776 4f3b383a46ae
output_tym: removed duplicate clauses;
src/Pure/Thy/html.ML
--- 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, "&sup2;")
      | "\\<threesuperior>" => (1.0, "&sup3;")
      | "\\<acute>" => (1.0, "&acute;")
-     | "\\<mu>" => (1.0, "&micro;")
      | "\\<paragraph>" => (1.0, "&para;")
      | "\\<cdot>" => (1.0, "&middot;")
      | "\\<cedilla>" => (1.0, "&cedil;")
@@ -93,7 +92,6 @@
      | "\\<threequarters>" => (1.0, "&frac34;")
      | "\\<questiondown>" => (1.0, "&iquest;")
      | "\\<times>" => (1.0, "&times;")
-     | "\\<emptyset>" => (1.0, "&Oslash;")
      | "\\<div>" => (1.0, "&divide;")
      | "\\<circ>" => (1.0, "&circ;")
      | "\\<Alpha>" => (1.0, "&Alpha;")