changeset 44887 | 7ca82df6e951 |
parent 41413 | 64cd30d6b0b8 |
child 54263 | c4159fe6fa46 |
--- a/src/HOL/Hahn_Banach/Bounds.thy Sun Sep 11 21:35:35 2011 +0200 +++ b/src/HOL/Hahn_Banach/Bounds.thy Sun Sep 11 22:55:26 2011 +0200 @@ -15,9 +15,8 @@ lemmas [elim?] = lub.least lub.upper -definition - the_lub :: "'a::order set \<Rightarrow> 'a" where - "the_lub A = The (lub A)" +definition the_lub :: "'a::order set \<Rightarrow> 'a" + where "the_lub A = The (lub A)" notation (xsymbols) the_lub ("\<Squnion>_" [90] 90)