tuned
authornipkow
Sat Jun 20 14:00:36 2009 +0200 (2009-06-20)
changeset 317317ffc1a901eea
parent 31730 d74830dc3e4a
child 31732 052399f580cf
child 31735 a00292a5587d
tuned
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Sat Jun 20 13:34:54 2009 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Sat Jun 20 14:00:36 2009 +0200
     1.3 @@ -51,9 +51,12 @@
     1.4  
     1.5  subsection{*Basic Properties of @{term Pi}*}
     1.6  
     1.7 -lemma Pi_I[simp]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
     1.8 +lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
     1.9    by (simp add: Pi_def)
    1.10  
    1.11 +lemma Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B"
    1.12 +by(simp add:Pi_def)
    1.13 +
    1.14  lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
    1.15    by (simp add: Pi_def)
    1.16