| changeset 35168 | 07b3112e464b |
| parent 35115 | 446c5063e4fd |
| child 35427 | ad039d29e01c |
| child 35525 | fa231b86cb1e |
--- a/src/HOLCF/Cfun.thy Wed Feb 17 08:05:16 2010 -0800 +++ b/src/HOLCF/Cfun.thy Wed Feb 17 08:19:46 2010 -0800 @@ -521,7 +521,7 @@ text {* results about strictify *} lemma cont_strictify1: "cont (\<lambda>f. if x = \<bottom> then \<bottom> else f\<cdot>x)" -by (simp add: cont_if) +by simp lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)" apply (rule monofunI)