src/HOLCF/Cont.thy
changeset 1274 ea0668a1c0ba
parent 1168 74be52691d62
child 1479 21eb5e156d91
--- a/src/HOLCF/Cont.thy	Fri Oct 06 16:17:08 1995 +0100
+++ b/src/HOLCF/Cont.thy	Fri Oct 06 17:25:24 1995 +0100
@@ -27,15 +27,15 @@
 
 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:                                 *)
-(*              monofun(f) & contlub(f)  <==> cont(f)                      *)
+(*              monofun(f) & contlub(f)  <==> cont(f)                       *)
 (* ------------------------------------------------------------------------ *)
 
 end