--- a/src/HOL/Real/HahnBanach/Bounds.thy Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Thu Apr 22 12:11:17 2004 +0200
@@ -14,13 +14,13 @@
lemmas [elim?] = lub.least lub.upper
+constdefs
+ the_lub :: "'a::order set \<Rightarrow> 'a"
+ "the_lub A \<equiv> The (lub A)"
+
syntax (xsymbols)
the_lub :: "'a::order set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
-constdefs
- the_lub :: "'a::order set \<Rightarrow> 'a"
- "\<Squnion>A \<equiv> The (lub A)"
-
lemma the_lub_equality [elim?]:
includes lub
shows "\<Squnion>A = (x::'a::order)"