replaced \<macron> by \<inverse>;
authorwenzelm
Tue, 09 Jan 2001 15:18:07 +0100
changeset 10831 024bdf8e52a4
parent 10830 d19f9f4c35ee
child 10832 e33b47e4246d
replaced \<macron> by \<inverse>;
src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Jan 09 15:17:08 2001 +0100
+++ b/src/Pure/Thy/html.ML	Tue Jan 09 15:18:07 2001 +0100
@@ -77,7 +77,7 @@
      | "\\<not>" => (1.0, "&not;")
      | "\\<hyphen>" => (1.0, "&shy;")
      | "\\<registered>" => (1.0, "&reg;")
-     | "\\<macron>" => (1.0, "&macr;")
+     | "\\<inverse>" => (1.0, "&macr;")
      | "\\<degree>" => (1.0, "&deg;")
      | "\\<plusminus>" => (1.0, "&plusmn;")
      | "\\<twosuperior>" => (1.0, "&sup2;")