src/HOL/Library/FuncSet.thy
changeset 31759 1e652c39d617
parent 31754 b5260f5272a4
child 31770 ba52fcfaec28
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Jun 22 20:59:33 2009 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 05:57:35 2009 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
     1.5    by (simp add: Pi_def)
     1.6  
     1.7 -lemma ballE [elim]:
     1.8 +lemma PiE [elim]:
     1.9    "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
    1.10  by(auto simp: Pi_def)
    1.11