author | huffman |
Sat, 04 Sep 2010 08:32:19 -0700 | |
changeset 39145 | 154fd9c06c63 |
parent 39144 | 23b1e6759359 |
child 39146 | 142f1425e074 |
child 39147 | 3c284a152bd6 |
--- a/src/HOLCF/Cfun.thy Sat Sep 04 07:35:56 2010 -0700 +++ b/src/HOLCF/Cfun.thy Sat Sep 04 08:32:19 2010 -0700 @@ -597,4 +597,12 @@ using g by (rule cont_fst_snd_D1) qed +text {* The simple version (suggested by Joachim Breitner) is needed if + the type of the defined term is not a cpo. *} + +lemma cont2cont_Let_simple [simp, cont2cont]: + assumes "\<And>y. cont (\<lambda>x. g x y)" + shows "cont (\<lambda>x. let y = t in g x y)" +unfolding Let_def using assms . + end