convert symbols to HTML 4.0 character entities,
convert some common remaining symbols to ASCII (e.g. lbrakk -> [|)

--- a/src/Pure/Thy/html.ML	Tue Apr 13 09:42:40 2004 +0200
+++ b/src/Pure/Thy/html.ML	Tue Apr 13 10:45:35 2004 +0200
@@ -95,11 +95,121 @@
      | "\\<times>" => (1.0, "&times;")
      | "\\<emptyset>" => (1.0, "&Oslash;")
      | "\\<div>" => (1.0, "&divide;")
+     | "\\<circ>" => (1.0, "&circ;")    
+     | "\\<Alpha>" => (1.0, "&Alpha;")
+     | "\\<Beta>" => (1.0, "&Beta;")
+     | "\\<Gamma>" => (1.0, "&Gamma;")
+     | "\\<Delta>" => (1.0, "&Delta;")
+     | "\\<Epsilon>" => (1.0, "&Epsilon;")
+     | "\\<Zeta>" => (1.0, "&Zeta;")
+     | "\\<Eta>" => (1.0, "&Eta;")
+     | "\\<Theta>" => (1.0, "&Theta;")
+     | "\\<Iota>" => (1.0, "&Iota;")
+     | "\\<Kappa>" => (1.0, "&Kappa;")
+     | "\\<Lambda>" => (1.0, "&Lambda;")
+     | "\\<Mu>" => (1.0, "&Mu;")
+     | "\\<Nu>" => (1.0, "&Nu;")
+     | "\\<Xi>" => (1.0, "&Xi;")
+     | "\\<Omicron>" => (1.0, "&Omicron;")
+     | "\\<Pi>" => (1.0, "&Pi;")
+     | "\\<Rho>" => (1.0, "&Rho;")
+     | "\\<Sigma>" => (1.0, "&Sigma;")
+     | "\\<Tau>" => (1.0, "&Tau;")
+     | "\\<Upsilon>" => (1.0, "&Upsilon;")
+     | "\\<Phi>" => (1.0, "&Phi;")
+     | "\\<Chi>" => (1.0, "&Chi;")
+     | "\\<Psi>" => (1.0, "&Psi;")
+     | "\\<Omega>" => (1.0, "&Omega;")
+     | "\\<alpha>" => (1.0, "&alpha;")
+     | "\\<beta>" => (1.0, "&beta;")
+     | "\\<gamma>" => (1.0, "&gamma;")
+     | "\\<delta>" => (1.0, "&delta;")
+     | "\\<epsilon>" => (1.0, "&epsilon;")
+     | "\\<zeta>" => (1.0, "&zeta;")
+     | "\\<eta>" => (1.0, "&eta;")
+     | "\\<theta>" => (1.0, "&thetasym;")
+     | "\\<iota>" => (1.0, "&iota;")
+     | "\\<kappa>" => (1.0, "&kappa;")
+     | "\\<lambda>" => (1.0, "&lambda;")
+     | "\\<mu>" => (1.0, "&mu;")
+     | "\\<nu>" => (1.0, "&nu;")
+     | "\\<xi>" => (1.0, "&xi;")
+     | "\\<omicron>" => (1.0, "&omicron;")
+     | "\\<pi>" => (1.0, "&pi;")
+     | "\\<rho>" => (1.0, "&rho;")
+     | "\\<sigma>" => (1.0, "&sigma;")
+     | "\\<tau>" => (1.0, "&tau;")
+     | "\\<upsilon>" => (1.0, "&upsilon;")
+     | "\\<phi>" => (1.0, "&phi;")
+     | "\\<chi>" => (1.0, "&chi;")
+     | "\\<psi>" => (1.0, "&psi;")
+     | "\\<omega>" => (1.0, "&omega;")
+     | "\\<buller>" => (1.0, "&bull;")
+     | "\\<dots>" => (1.0, "&hellip;")
+     | "\\<Re>" => (1.0, "&real;")
+     | "\\<Im>" => (1.0, "&image;")
+     | "\\<wp>" => (1.0, "&weierp;")
+     | "\\<forall>" => (1.0, "&forall;")
+     | "\\<partial>" => (1.0, "&part;")
+     | "\\<exists>" => (1.0, "&exist;")
+     | "\\<emptyset>" => (1.0, "&empty;")
+     | "\\<nabla>" => (1.0, "&nabla;")
+     | "\\<in>" => (1.0, "&isin;")
+     | "\\<notin>" => (1.0, "&notin;")
+     | "\\<star>" => (1.0, "&lowast;")
+     | "\\<propto>" => (1.0, "&prop;")
+     | "\\<infinity>" => (1.0, "&infin;")
+     | "\\<angle>" => (1.0, "&ang;")
+     | "\\<and>" => (1.0, "&and;")     
+     | "\\<or>" => (1.0, "&or;")
+     | "\\<inter>" => (1.0, "&cap;")
+     | "\\<union>" => (1.0, "&cup;")
+     | "\\<sim>" => (1.0, "&sim;")
+     | "\\<cong>" => (1.0, "&cong;")
+     | "\\<approx>" => (1.0, "&asymp;")
+     | "\\<noteq>" => (1.0, "&ne;")
+     | "\\<equiv>" => (1.0, "&equiv;")
+     | "\\<le>" => (1.0, "&le;")
+     | "\\<ge>" => (1.0, "&ge;")
+     | "\\<subset>" => (1.0, "&sub;")
+     | "\\<supset>" => (1.0, "&sup;")
+     | "\\<subseteq>" => (1.0, "&sube;")
+     | "\\<supseteq>" => (1.0, "&supe;")
+     | "\\<oplus>" => (1.0, "&oplus;")
+     | "\\<otimes>" => (1.0, "&otimes;")
+     | "\\<bottom>" => (1.0, "&perp;")
+     | "\\<lceil>" => (1.0, "&lceil;")
+     | "\\<rceil>" => (1.0, "&rceil;")
+     | "\\<lfloor>" => (1.0, "&lfloor;")
+     | "\\<rfloor>" => (1.0, "&rfloor;")
+     | "\\<langle>" => (1.0, "&lang;")
+     | "\\<rangle>" => (1.0, "&rang;")
+     | "\\<lozenge>" => (1.0, "&loz;")
+     | "\\<spadesuit>" => (1.0, "&spades;")
+     | "\\<clubsuit>" => (1.0, "&clubs;")
+     | "\\<heartsuit>" => (1.0, "&hearts;")
+     | "\\<diamondsuit>" => (1.0, "&diams;")
+
+     | "\\<lbrakk>" => (2.0, "[|")
+     | "\\<rbrakk>" => (2.0, "|]")
+     | "\\<Longrightarrow>" => (3.0, "==&gt;")
+     | "\\<Rightarrow>" => (3.0, "=&gt;")
+     | "\\<And>" => (2.0, "!!")
+     | "\\<Colon>" => (2.0, "::")
+     | "\\<lparr>" => (2.0, "(|")
+     | "\\<rparr>" => (2.0, "|)")
+     | "\\<longleftrightarrow>" => (3.0, "&lt;-&gt;")
+     | "\\<longrightarrow>" => (3.0, "--&gt;")
+     | "\\<rightarrow>" => (2.0, "-&gt;")
+     | "\\<rightleftharpoons>" => (2.0, "==")
+     | "\\<rightharpoonup>" => (2.0, "=&gt;")
+     | "\\<leftharpoondown>" => (2.0, "&lt;=")
+
      | "\\<^bsub>" => (0.0, "<sub>")
      | "\\<^esub>" => (0.0, "</sub>")
      | "\\<^bsup>" => (0.0, "<sup>")
      | "\\<^esup>" => (0.0, "</sup>")
-(* keep \<^sub> etc, so it does not get destroyed by default case *)
+(* keep \<^sub> etc, so they are not destroyed by default case *)
      | "\\<^sup>" => (0.0, "\\<^sup>")
      | "\\<^sub>" => (0.0, "\\<^sub>")
      | "\\<^isup>" => (0.0, "\\<^isup>")