# HG changeset patch
# User nipkow
# Date 1245499236 -7200
# Node ID 7ffc1a901eea94b14aa12df95fdb7f44186c2311
# Parent  d74830dc3e4ab51ad3e3e609aebe2a516834687f
tuned

diff -r d74830dc3e4a -r 7ffc1a901eea src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sat Jun 20 13:34:54 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sat Jun 20 14:00:36 2009 +0200
@@ -51,9 +51,12 @@
 
 subsection{*Basic Properties of @{term Pi}*}
 
-lemma Pi_I[simp]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
+lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
   by (simp add: Pi_def)
 
+lemma Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B"
+by(simp add:Pi_def)
+
 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
   by (simp add: Pi_def)