# HG changeset patch
# User huffman
# Date 1213301647 -7200
# Node ID e1e9b210d69975b5b25545395df2705fb4452431
# Parent  51f3f3557ef4ee70fcba34b5c044a5426cb25a25
remove unnecessary import of Ffun;
add lemma admD2

diff -r 51f3f3557ef4 -r e1e9b210d699 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Thu Jun 12 22:12:27 2008 +0200
+++ b/src/HOLCF/Adm.thy	Thu Jun 12 22:14:07 2008 +0200
@@ -6,7 +6,7 @@
 header {* Admissibility and compactness *}
 
 theory Adm
-imports Ffun
+imports Cont
 begin
 
 defaultsort cpo
@@ -24,6 +24,9 @@
 lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
 unfolding adm_def by fast
 
+lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)"
+unfolding adm_def by fast
+
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 by (rule admI, erule spec)