# HG changeset patch
# User huffman
# Date 1268007121 28800
# Node ID a17bc4cec23ad6a5a8137f979c3bb87f41bd703a
# Parent  9617aeca7147d4b4dd5dfd1284a266611323a4a3
add simp rule LAM_strict

diff -r 9617aeca7147 -r a17bc4cec23a src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sun Mar 07 13:34:53 2010 -0800
+++ b/src/HOLCF/Cfun.thy	Sun Mar 07 16:12:01 2010 -0800
@@ -126,9 +126,12 @@
 lemma Rep_CFun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
 by (simp add: Rep_CFun_strict)
 
+lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
+by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
-by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+by simp
 
 subsection {* Basic properties of continuous functions *}