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.
merged
authornipkow
Tue, 23 Jun 2009 05:58:00 +0200
changeset 31760 05e3e5980677
parent 31758 3edd5f813f01 (current diff)
parent 31759 1e652c39d617 (diff)
child 31761 3585bebe49a8
child 31766 f767c5b1702e
merged
--- 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)
isabelle