src/HOLCF/Cont.thy
 changeset 1479 21eb5e156d91 parent 1274 ea0668a1c0ba child 2838 2e908f29bc3d
```--- a/src/HOLCF/Cont.thy	Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cont.thy	Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/cont.thy
+(*  Title:      HOLCF/cont.thy
ID:         \$Id\$
-    Author: 	Franz Regensburger
+    Author:     Franz Regensburger

@@ -19,19 +19,19 @@
default pcpo

consts
-	monofun :: "('a::po => 'b::po) => bool"	(* monotonicity    *)
-	contlub	:: "('a => 'b) => bool"		(* first cont. def *)
-	cont	:: "('a => 'b) => bool"		(* secnd cont. def *)
+        monofun :: "('a::po => 'b::po) => bool" (* monotonicity    *)
+        contlub :: "('a => 'b) => bool"         (* first cont. def *)
+        cont    :: "('a => 'b) => bool"         (* secnd cont. def *)

defs

-monofun		"monofun(f) == ! x y. x << y --> f(x) << f(y)"
+monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"

-contlub		"contlub(f) == ! Y. is_chain(Y) -->
-				f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
+contlub         "contlub(f) == ! Y. is_chain(Y) -->
+                                f(lub(range(Y))) = lub(range(% i.f(Y(i))))"

-cont		"cont(f)   == ! Y. is_chain(Y) -->
-				range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+cont            "cont(f)   == ! Y. is_chain(Y) -->
+                                range(% i.f(Y(i))) <<| f(lub(range(Y)))"

(* ------------------------------------------------------------------------ *)
(* the main purpose of cont.thy is to show:                                 *)```