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