# HG changeset patch
# User haftmann
# Date 1552231005 0
# Node ID 06f204a2f3c254f8bd35c512772958699f562a7f
# Parent  6f5bd59f75f4f32d6cd2bcdc3d30dc9bd69c6b9c
dropped superfluous declaration attribute

diff -r 6f5bd59f75f4 -r 06f204a2f3c2 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Mar 13 13:46:16 2019 +0100
+++ b/src/HOL/Relation.thy	Sun Mar 10 15:16:45 2019 +0000
@@ -523,7 +523,7 @@
 subsubsection \<open>The identity relation\<close>
 
 definition Id :: "'a rel"
-  where [code del]: "Id = {p. \<exists>x. p = (x, x)}"
+  where "Id = {p. \<exists>x. p = (x, x)}"
 
 lemma IdI [intro]: "(a, a) \<in> Id"
   by (simp add: Id_def)