1.1 --- a/src/HOLCF/Cont.thy	Sat May 22 19:17:18 2010 -0700
     1.2 +++ b/src/HOLCF/Cont.thy	Sun May 23 19:30:14 2010 -0700
     1.3 @@ -178,7 +178,7 @@
     1.4  
     1.5  text {* if-then-else is continuous *}
     1.6  
     1.7 -lemma cont_if [simp]:
     1.8 +lemma cont_if [simp, cont2cont]:
     1.9    "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
    1.10  by (induct b) simp_all
    1.11  

     2.1 --- a/src/HOLCF/Lift.thy	Sat May 22 19:17:18 2010 -0700
     2.2 +++ b/src/HOLCF/Lift.thy	Sun May 23 19:30:14 2010 -0700
     2.3 @@ -137,7 +137,7 @@
     2.4  apply (simp add: below_fun_ext)
     2.5  done
     2.6  
     2.7 -lemma cont2cont_flift1 [simp]:
     2.8 +lemma cont2cont_flift1 [simp, cont2cont]:
     2.9    "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
    2.10  apply (rule cont_flift1 [THEN cont2cont_app3])
    2.11  apply simp