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