# HG changeset patch
# User kleing
# Date 1081929205 -7200
# Node ID 726f6761c5629e23a00f962fb464f6736030d331
# Parent  31ae4a47267c3d54934da3a6f89bc5c53bddb7d2
prod and sum

diff -r 31ae4a47267c -r 726f6761c562 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Apr 13 23:08:12 2004 +0200
+++ b/src/Pure/Thy/html.ML	Wed Apr 14 09:53:25 2004 +0200
@@ -156,6 +156,8 @@
      | "\\<nabla>" => (1.0, "&nabla;")
      | "\\<in>" => (1.0, "&isin;")
      | "\\<notin>" => (1.0, "&notin;")
+     | "\\<prod>" => (1.0, "&prod;")
+     | "\\<sum>" => (1.0, "&sum;")
      | "\\<star>" => (1.0, "&lowast;")
      | "\\<propto>" => (1.0, "&prop;")
      | "\\<infinity>" => (1.0, "&infin;")