# HG changeset patch
# User wenzelm
# Date 1413882796 -7200
# Node ID 5d452cf4bce794c60add6c2a717a9a7a5c925c41
# Parent  c434e37f290e4527253c94447284237496f69f24
tuned;

diff -r c434e37f290e -r 5d452cf4bce7 src/HOL/Hahn_Banach/Bounds.thy
--- a/src/HOL/Hahn_Banach/Bounds.thy	Tue Oct 21 10:58:19 2014 +0200
+++ b/src/HOL/Hahn_Banach/Bounds.thy	Tue Oct 21 11:13:16 2014 +0200
@@ -15,12 +15,9 @@
 
 lemmas [elim?] = lub.least lub.upper
 
-definition the_lub :: "'a::order set \<Rightarrow> 'a"
+definition the_lub :: "'a::order set \<Rightarrow> 'a"  ("\<Squnion>_" [90] 90)
   where "the_lub A = The (lub A)"
 
-notation (xsymbols)
-  the_lub  ("\<Squnion>_" [90] 90)
-
 lemma the_lub_equality [elim?]:
   assumes "lub A x"
   shows "\<Squnion>A = (x::'a::order)"
diff -r c434e37f290e -r 5d452cf4bce7 src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Tue Oct 21 10:58:19 2014 +0200
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Tue Oct 21 11:13:16 2014 +0200
@@ -102,7 +102,7 @@
 
 definition
   norm_pres_extensions ::
-    "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
+    "'a::{plus,minus,uminus,zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
       \<Rightarrow> 'a graph set"
 where
   "norm_pres_extensions E p F f
diff -r c434e37f290e -r 5d452cf4bce7 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Tue Oct 21 10:58:19 2014 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Tue Oct 21 11:13:16 2014 +0200
@@ -143,7 +143,7 @@
   scalar multiples of @{text x}.
 \<close>
 
-definition lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
+definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
   where "lin x = {a \<cdot> x | a. True}"
 
 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
diff -r c434e37f290e -r 5d452cf4bce7 src/HOL/Hahn_Banach/Vector_Space.thy
--- 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>