# 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: "\adm P; adm Q\ \ adm (\x. P x \ Q x)" by (fast intro: admI elim: admD) -lemma adm_all: "(\y. adm (P y)) \ adm (\x. \y. P y x)" +lemma adm_all: "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)" by (fast intro: admI elim: admD) -lemma adm_ball: "(\y. y \ A \ adm (P y)) \ adm (\x. \y\A. P y x)" +lemma adm_ball: "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)" by (fast intro: admI elim: admD) text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *}