diff -r f8a615f3bb31 -r ed657432b8b9 src/HOLCF/Cont.thy
--- 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 *}