changeset 40923 | be80c93ac0a2 |
parent 36772 | ef97c5006840 |
child 41056 | dcec9bc71ee9 |
--- a/src/HOL/Relation.thy Fri Dec 03 08:40:47 2010 +0100 +++ b/src/HOL/Relation.thy Fri Dec 03 08:40:47 2010 +0100 @@ -132,6 +132,11 @@ lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" by blast +lemma Id_on_def'[nitpick_def, code]: + "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)" +by (auto simp add: fun_eq_iff + elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def]) + lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" by blast