| changeset 26452 | ed657432b8b9 |
| parent 26027 | 87cb69d27558 |
| child 27413 | 3154f3765cc7 |
--- a/src/HOLCF/Cont.thy Thu Mar 27 19:22:24 2008 +0100 +++ b/src/HOLCF/Cont.thy Thu Mar 27 19:49:24 2008 +0100 @@ -186,7 +186,8 @@ text {* if-then-else is continuous *} -lemma cont_if: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" +lemma cont_if [simp]: + "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" by (induct b) simp_all subsection {* Finite chains and flat pcpos *}