diff -r 6960ec882bca -r ea0668a1c0ba src/HOLCF/Cont.thy --- 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