# HG changeset patch
# User huffman
# Date 1257449790 28800
# Node ID 3496616b2171685437e43ec0d901b9520ed153a4
# Parent  f5d95787224fe0ca82dd4e00e9e6cbe3f024a188
lemma deflation_strict

diff -r f5d95787224f -r 3496616b2171 src/HOLCF/Deflation.thy
--- 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)