fixed name
authornipkow
Tue Jun 23 05:57:35 2009 +0200 (2009-06-23)
changeset 317591e652c39d617
parent 31755 78529fc872b1
child 31760 05e3e5980677
fixed name
src/HOL/Library/FuncSet.thy
     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