# HG changeset patch
# User huffman
# Date 1283614339 25200
# Node ID 154fd9c06c6304438461f97dee8d3790160b9832
# Parent  23b1e67593596bfa8ce2679b5269fd21c483d591
add lemma cont2cont_Let_simple

diff -r 23b1e6759359 -r 154fd9c06c63 src/HOLCF/Cfun.thy
--- 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