# HG changeset patch
# User huffman
# Date 1127408794 -7200
# Node ID df8b2f0e462e07c3c6b2bb525d90e7b42da29711
# Parent  f12d7ac88eb4a128a034c48c55f6dda91e167873
added theorem adm_ball

diff -r f12d7ac88eb4 -r df8b2f0e462e src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Thu Sep 22 19:06:05 2005 +0200
+++ b/src/HOLCF/Adm.thy	Thu Sep 22 19:06:34 2005 +0200
@@ -93,6 +93,11 @@
 
 lemmas adm_all2 = adm_all [rule_format]
 
+lemma adm_ball: "\<forall>y\<in>A. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P y x)"
+by (fast intro: admI elim: admD)
+
+lemmas adm_ball2 = adm_ball [rule_format]
+
 lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
 apply (rule admI)
 apply (simp add: cont2contlubE)
@@ -224,6 +229,8 @@
 val adm_not_less = thm "adm_not_less";
 val adm_all = thm "adm_all";
 val adm_all2 = thm "adm_all2";
+val adm_ball = thm "adm_ball";
+val adm_ball2 = thm "adm_ball2";
 val adm_subst = thm "adm_subst";
 val adm_UU_not_less = thm "adm_UU_not_less";
 val adm_not_UU = thm "adm_not_UU";