author | haftmann |
Sat, 24 Dec 2011 15:53:09 +0100 | |
changeset 45967 | 76cf71ed15c7 |
parent 45966 | 03ce2b2a29a2 |
child 45968 | e8fa5090fa04 |
--- a/src/HOL/Relation.thy Sat Dec 24 15:53:09 2011 +0100 +++ b/src/HOL/Relation.thy Sat Dec 24 15:53:09 2011 +0100 @@ -132,7 +132,7 @@ lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" by blast -lemma Id_on_def' [nitpick_unfold, code]: +lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" by auto