src/HOLCF/Fixrec.thy
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