# HG changeset patch
# User huffman
# Date 1158254290 -7200
# Node ID 1c49d9f4410e52dbc7e6c3e8dfdcd8f80d082685
# Parent  b6b49903db7ef694330b13b278579e0a248ee88f
fixed syntax clash with Real/RealVector

diff -r b6b49903db7e -r 1c49d9f4410e src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Sep 14 15:51:20 2006 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Sep 14 19:18:10 2006 +0200
@@ -15,8 +15,6 @@
   definite, absolute homogenous and subadditive.
 *}
 
-no_syntax norm :: "'a::norm \<Rightarrow> real" ("\<parallel>_\<parallel>")   (* FIXME clash with Real/RealVector.thy *)
-
 locale norm_syntax =
   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")