dropped superfluous declaration attribute
authorhaftmann
Sun Mar 10 15:16:45 2019 +0000 (6 weeks ago ago)
changeset 7008606f204a2f3c2
parent 70085 6f5bd59f75f4
child 70087 55534affe445
dropped superfluous declaration attribute
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Wed Mar 13 13:46:16 2019 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -523,7 +523,7 @@
     1.4  subsubsection \<open>The identity relation\<close>
     1.5  
     1.6  definition Id :: "'a rel"
     1.7 -  where [code del]: "Id = {p. \<exists>x. p = (x, x)}"
     1.8 +  where "Id = {p. \<exists>x. p = (x, x)}"
     1.9  
    1.10  lemma IdI [intro]: "(a, a) \<in> Id"
    1.11    by (simp add: Id_def)