Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed name
authornipkow
Tue, 23 Jun 2009 05:57:35 +0200
changeset 31759 1e652c39d617
parent 31755 78529fc872b1
child 31760 05e3e5980677
fixed name
src/HOL/Library/FuncSet.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/FuncSet.thy	Mon Jun 22 20:59:33 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 05:57:35 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)
isabelle