--- 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