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