# HG changeset patch
# User nipkow
# Date 1401354682 -7200
# Node ID de33f3965ca66729d11c97a63f78f8b6cd2e30e3
# Parent  95e5a633a18f90c6093c402133b0948024a10bf1
typo

diff -r 95e5a633a18f -r de33f3965ca6 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: