src/HOLCF/Porder.thy
changeset 2394 91d8abf108be
parent 2291 fbd14a05fb88
child 2640 ee4dfce170a0
--- a/src/HOLCF/Porder.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Porder.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -18,6 +18,18 @@
         max_in_chain :: "[nat,nat=>'a::po]=>bool"
         finite_chain :: "(nat=>'a::po)=>bool"
 
+syntax
+
+  "@LUB"	:: "(('b::term) => 'a) => 'a"	(binder "LUB " 10)
+
+translations
+
+  "LUB x. t"	== "lub(range(%x.t))"
+
+syntax (symbols)
+
+  "LUB "	:: "[idts, 'a] => 'a"		("(3\\<Squnion>_./ _)"[0,10] 10)
+
 defs
 
 (* class definitions *)
@@ -27,23 +39,20 @@
 
 
 (* Arbitrary chains are total orders    *)                  
-is_tord         "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
+is_tord         "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
 
 (* Here we use countable chains and I prefer to code them as functions! *)
-is_chain        "is_chain(F) == (! i.F(i) << F(Suc(i)))"
+is_chain        "is_chain F == (! i.F(i) << F(Suc(i)))"
 
 (* finite chains, needed for monotony of continouous functions *)
 
 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
 
-finite_chain_def "finite_chain(C) == is_chain(C) & (? i. max_in_chain i C)"
+finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
 
 rules
 
-lub             "lub(S) = (@x. S <<| x)"
-
-(* start 8bit 1 *)
-(* end 8bit 1 *)
+lub             "lub S = (@x. S <<| x)"
 
 end