diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Fix.thy --- a/src/HOLCF/Fix.thy Wed Mar 26 13:44:05 1997 +0100 +++ b/src/HOLCF/Fix.thy Wed Mar 26 17:58:48 1997 +0100 @@ -15,10 +15,10 @@ iterate :: "nat=>('a->'a)=>'a=>'a" Ifix :: "('a->'a)=>'a" fix :: "('a->'a)->'a" -adm :: "('a=>bool)=>bool" +adm :: "('a::cpo=>bool)=>bool" admw :: "('a=>bool)=>bool" -chain_finite :: "'a=>bool" -flat :: "'a=>bool" (* should be called flat, for consistency *) +chain_finite :: "'a::cpo=>bool" +flat :: "'a=>bool" defs @@ -32,8 +32,8 @@ admw_def "admw P == !F. (!n.P (iterate n F UU)) --> P (lub(range (%i. iterate i F UU)))" -chain_finite_def "chain_finite (x::'a)== - !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)" +chain_finite_def "chain_finite (x::'a::cpo)== + !Y. is_chain (Y::nat=>'a::cpo) --> (? n.max_in_chain n Y)" flat_def "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"