changeset 14565 | c6dc17aab88a |
parent 13515 | a6a7025fd7e8 |
child 14710 | 247615bfffb8 |
1.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Apr 14 13:28:46 2004 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Apr 14 14:13:05 2004 +0200 1.3 @@ -20,6 +20,8 @@ 1.4 1.5 syntax (xsymbols) 1.6 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70) 1.7 +syntax (HTML output) 1.8 + prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70) 1.9 1.10 1.11 subsection {* Vector space laws *}