--- a/src/HOL/Hahn_Banach/Vector_Space.thy Tue Oct 21 10:58:19 2014 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Tue Oct 21 11:13:16 2014 +0200
@@ -17,12 +17,7 @@
\<close>
consts
- prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
-
-notation (xsymbols)
- prod (infixr "\<cdot>" 70)
-notation (HTML output)
- prod (infixr "\<cdot>" 70)
+ prod :: "real \<Rightarrow> 'a::{plus,minus,zero} \<Rightarrow> 'a" (infixr "\<cdot>" 70)
subsection \<open>Vector space laws\<close>