changeset 14565 | c6dc17aab88a |
parent 13515 | a6a7025fd7e8 |
child 14710 | 247615bfffb8 |
--- 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 *}