# HG changeset patch
# User huffman
# Date 1213976596 -7200
# Node ID 784620cccb80b12806496b3b75840558b1eebf06
# Parent  c49d427867aab967fd5b6c7069716a115223d576
tweak lemmas adm_all and adm_ball

diff -r c49d427867aa -r 784620cccb80 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Thu Jun 19 22:50:58 2008 +0200
+++ b/src/HOLCF/Adm.thy	Fri Jun 20 17:43:16 2008 +0200
@@ -55,10 +55,10 @@
 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
 by (fast intro: admI elim: admD)
 
-lemma adm_all: "(\<And>y. adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
+lemma adm_all: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
 by (fast intro: admI elim: admD)
 
-lemma adm_ball: "(\<And>y. y \<in> A \<Longrightarrow> adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P y x)"
+lemma adm_ball: "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
 by (fast intro: admI elim: admD)
 
 text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *}