src/HOLCF/Porder.thy

--- a/src/HOLCF/Porder.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Porder.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -43,6 +43,13 @@
 lub             "lub(S) = (@x. S <<| x)"
 
 (* start 8bit 1 *)
+
+syntax
+  "Glub"        :: "[pttrn, 'a] => 'a"               ("(3×_./ _)" 10)
+
+translations
+  "×x.t"	== "lub(range(%x.t))"
+
 (* end 8bit 1 *)
 
 end