src/HOL/Library/FuncSet.thy
changeset 31770 ba52fcfaec28
parent 31759 1e652c39d617
parent 31769 d5f39775edd2
child 32988 d1d4d7a08a66
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jun 23 10:22:11 2009 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 11:32:12 2009 +0200
     1.3 @@ -67,6 +67,9 @@
     1.4    "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     1.5  by(auto simp: Pi_def)
     1.6  
     1.7 +lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
     1.8 +  by (auto intro: Pi_I)
     1.9 +
    1.10  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
    1.11    by (simp add: Pi_def)
    1.12