# HG changeset patch
# User wenzelm
# Date 1085167144 -7200
# Node ID 65c22319829f0ad3321d28f866ac41a92bbe7ad1
# Parent  d747c32e85e12892ef83919c99b5c3cc3b432cf2
output_tym: removed duplicate clauses;

diff -r d747c32e85e1 -r 65c22319829f 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;")