| changeset 38656 | d5d342611edb |
| parent 33271 | 7be66dee1a5a |
| child 39198 | f967a16dfcdd |
--- a/src/HOL/Library/FuncSet.thy Mon Aug 23 17:46:13 2010 +0200 +++ b/src/HOL/Library/FuncSet.thy Mon Aug 23 19:35:57 2010 +0200 @@ -67,6 +67,10 @@ "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q" by(auto simp: Pi_def) +lemma Pi_cong: + "(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B" + by (auto simp: Pi_def) + lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" by (auto intro: Pi_I)