author | haftmann |
Sun, 10 Mar 2019 15:16:45 +0000 | |
changeset 69905 | 06f204a2f3c2 |
parent 69904 | 6f5bd59f75f4 |
child 69906 | 55534affe445 |
--- 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)