| changeset 37099 | 3636b08cbf51 |
| parent 37079 | 0cd15d8c90a0 |
| child 40004 | 9f6ed6840e8d |
--- a/src/HOLCF/Cont.thy Sat May 22 19:17:18 2010 -0700 +++ b/src/HOLCF/Cont.thy Sun May 23 19:30:14 2010 -0700 @@ -178,7 +178,7 @@ text {* if-then-else is continuous *} -lemma cont_if [simp]: +lemma cont_if [simp, cont2cont]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" by (induct b) simp_all