author | nipkow |
Thu, 29 May 2014 11:11:22 +0200 | |
changeset 57111 | de33f3965ca6 |
parent 57110 | 95e5a633a18f |
child 57112 | 70395c65c0e3 |
child 57113 | 7e95523302e6 |
--- a/src/HOL/Relation.thy Wed May 28 19:18:18 2014 +0200 +++ b/src/HOL/Relation.thy Thu May 29 11:11:22 2014 +0200 @@ -456,7 +456,7 @@ "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" by (simp add: single_valued_def) -lemma simgle_valued_empty[simp]: "single_valued {}" +lemma single_valued_empty[simp]: "single_valued {}" by(simp add: single_valued_def) lemma single_valued_subset: