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