changeset 21210 | c17fd2df4e9e |
parent 19736 | d8d0f8f51d69 |
child 23378 | 1d138d6bb461 |
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Nov 07 11:47:57 2006 +0100 @@ -18,9 +18,9 @@ consts prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70) -const_syntax (xsymbols) +notation (xsymbols) prod (infixr "\<cdot>" 70) -const_syntax (HTML output) +notation (HTML output) prod (infixr "\<cdot>" 70)