src/HOLCF/Cfun2.ML
changeset 297 5ef75ff3baeb
parent 243 c22b85994e17
child 892 d0dc8d057929
     1.1 --- a/src/HOLCF/Cfun2.ML	Thu Mar 24 13:25:12 1994 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Thu Mar 24 13:36:34 1994 +0100
     1.3 @@ -216,7 +216,7 @@
     1.4  is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
     1.5  *)
     1.6  
     1.7 -val cpo_fun = prove_goal Cfun2.thy 
     1.8 +val cpo_cfun = prove_goal Cfun2.thy 
     1.9    "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
    1.10  (fn prems =>
    1.11  	[