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