src/HOL/Relation.thy
changeset 48253 4410a709913c
parent 47937 70375fa2679d
child 48620 fc9be489e2fb
     1.1 --- a/src/HOL/Relation.thy	Thu Jul 12 21:46:11 2012 +1000
     1.2 +++ b/src/HOL/Relation.thy	Thu Jul 12 16:22:33 2012 +0200
     1.3 @@ -427,7 +427,7 @@
     1.4  
     1.5  definition Id :: "'a rel"
     1.6  where
     1.7 -  "Id = {p. \<exists>x. p = (x, x)}"
     1.8 +  [code del]: "Id = {p. \<exists>x. p = (x, x)}"
     1.9  
    1.10  lemma IdI [intro]: "(a, a) : Id"
    1.11    by (simp add: Id_def)