| changeset 69905 | 06f204a2f3c2 |
| parent 69593 | 3dda49e08b9d |
| child 71404 | f2b783abfbe7 |
--- 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)