--- 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
--- a/src/HOLCF/Lift.thy Sat May 22 19:17:18 2010 -0700
+++ b/src/HOLCF/Lift.thy Sun May 23 19:30:14 2010 -0700
@@ -137,7 +137,7 @@
apply (simp add: below_fun_ext)
done
-lemma cont2cont_flift1 [simp]:
+lemma cont2cont_flift1 [simp, cont2cont]:
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
apply (rule cont_flift1 [THEN cont2cont_app3])
apply simp