dropped obsolete code equation for Id
authorhaftmann
Sat Dec 24 15:53:09 2011 +0100 (2011-12-24)
changeset 4596776cf71ed15c7
parent 45966 03ce2b2a29a2
child 45968 e8fa5090fa04
dropped obsolete code equation for Id
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Sat Dec 24 15:53:09 2011 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sat Dec 24 15:53:09 2011 +0100
     1.3 @@ -132,7 +132,7 @@
     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_unfold, code]:
     1.8 +lemma Id_on_def' [nitpick_unfold]:
     1.9    "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
    1.10  by auto
    1.11