# HG changeset patch
# User nipkow
# Date 1245729480 -7200
# Node ID 05e3e5980677977c71fcd5ca69c73fd8e2ebed29
# Parent  3edd5f813f01c8a82f86f16847e5d7ecfdff1799# Parent  1e652c39d617be88fd2fe394a76633dbd27f2dbb
merged

diff -r 3edd5f813f01 -r 05e3e5980677 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Jun 22 23:48:24 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 05:58:00 2009 +0200
@@ -63,7 +63,7 @@
 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
   by (simp add: Pi_def)
 
-lemma ballE [elim]:
+lemma PiE [elim]:
   "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
 by(auto simp: Pi_def)