src/HOL/Relation.thy
changeset 44278 1220ecb81e8f
parent 41792 ff3cb0c418b7
child 44921 58eef4843641
     1.1 --- a/src/HOL/Relation.thy	Thu Aug 18 13:25:17 2011 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Aug 18 13:55:26 2011 +0200
     1.3 @@ -133,9 +133,8 @@
     1.4  by blast
     1.5  
     1.6  lemma Id_on_def' [nitpick_unfold, code]:
     1.7 -  "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
     1.8 -by (auto simp add: fun_eq_iff
     1.9 -  elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
    1.10 +  "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
    1.11 +by auto
    1.12  
    1.13  lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
    1.14  by blast