--- 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)