typo
authornipkow
Thu, 29 May 2014 11:11:22 +0200
changeset 57111 de33f3965ca6
parent 57110 95e5a633a18f
child 57112 70395c65c0e3
child 57113 7e95523302e6
typo
src/HOL/Relation.thy
--- 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: