| changeset 31769 | d5f39775edd2 |
| parent 31731 | 7ffc1a901eea |
| child 31770 | ba52fcfaec28 |
--- a/src/HOL/Library/FuncSet.thy Tue Jun 23 11:31:27 2009 +0200 +++ b/src/HOL/Library/FuncSet.thy Tue Jun 23 11:31:28 2009 +0200 @@ -63,6 +63,9 @@ lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x" by (simp add: 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)