diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -20,6 +20,8 @@
 
 syntax (xsymbols)
   prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
+syntax (HTML output)
+  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
 
 
 subsection {* Vector space laws *}