src/HOLCF/Lift.thy

--- a/src/HOLCF/Lift.thy	Mon May 01 01:21:23 2006 +0200
+++ b/src/HOLCF/Lift.thy	Mon May 01 01:22:31 2006 +0200
@@ -173,6 +173,9 @@
 lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
 by (erule lift_definedE, simp)
 
+lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
+by (cases x, simp_all)
+
 text {*
   \medskip Extension of @{text cont_tac} and installation of simplifier.
 *}