# HG changeset patch
# User huffman
# Date 1146439351 -7200
# Node ID 873dad2d8a6d57fe00624d38c5d83997b9725ebe
# Parent  8134024166b83bd6ee1ae4e1b6b1dc743eaeea59
add theorem flift2_defined_iff

diff -r 8134024166b8 -r 873dad2d8a6d 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.
 *}