--- a/src/HOLCF/Porder.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOLCF/Porder.thy Sun Nov 26 18:07:16 2006 +0100
@@ -87,14 +87,13 @@
lub :: "'a set \<Rightarrow> 'a::po"
"lub S \<equiv> THE x. S <<| x"
-syntax
- "@LUB" :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "LUB " 10)
+abbreviation
+ Lub (binder "LUB " 10) where
+ "LUB n. t n == lub (range t)"
-syntax (xsymbols)
- "LUB " :: "[idts, 'a] \<Rightarrow> 'a" ("(3\<Squnion>_./ _)" [0,10] 10)
+notation (xsymbols)
+ Lub (binder "\<Squnion> " 10)
-translations
- "\<Squnion>n. t" == "lub(CONST range(\<lambda>n. t))"
text {* lubs are unique *}