--- 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)"
--- 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
--- 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"
--- 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>