src/HOLCF/Fixrec.thy
changeset 29530 9905b660612b
parent 29322 ae6f2b1559fa
child 30131 6be1be402ef0
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Jan 14 13:47:14 2009 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Wed Jan 14 17:11:29 2009 -0800
     1.3 @@ -55,6 +55,7 @@
     1.4    "maybe_when\<cdot>f\<cdot>r\<cdot>fail = f"
     1.5    "maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x"
     1.6  by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe
     1.7 +                  cont2cont_LAM
     1.8                    cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
     1.9  
    1.10  translations