src/HOL/HOLCF/ex/Letrec.thy
changeset 45788 9049b24959de
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/ex/Letrec.thy	Thu Dec 08 13:25:54 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/ex/Letrec.thy	Thu Dec 08 13:46:04 2011 +0100
     1.3 @@ -8,10 +8,8 @@
     1.4  imports HOLCF
     1.5  begin
     1.6  
     1.7 -default_sort pcpo
     1.8 -
     1.9  definition
    1.10 -  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
    1.11 +  CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where
    1.12    "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
    1.13  
    1.14  nonterminal recbinds and recbindt and recbind