lemma deflation_strict

--- a/src/HOLCF/Deflation.thy	Thu Nov 05 14:37:39 2009 +0100
+++ b/src/HOLCF/Deflation.thy	Thu Nov 05 11:36:30 2009 -0800
@@ -55,6 +55,9 @@
 
 end
 
+lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
+by (rule deflation.below [THEN UU_I])
+
 lemma adm_deflation: "adm (\<lambda>d. deflation d)"
 by (simp add: deflation_def)