typo
authornipkow
Thu May 29 11:11:22 2014 +0200 (2014-05-29)
changeset 57111de33f3965ca6
parent 57110 95e5a633a18f
child 57112 70395c65c0e3
child 57113 7e95523302e6
typo
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Wed May 28 19:18:18 2014 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu May 29 11:11:22 2014 +0200
     1.3 @@ -456,7 +456,7 @@
     1.4    "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
     1.5    by (simp add: single_valued_def)
     1.6  
     1.7 -lemma simgle_valued_empty[simp]: "single_valued {}"
     1.8 +lemma single_valued_empty[simp]: "single_valued {}"
     1.9  by(simp add: single_valued_def)
    1.10  
    1.11  lemma single_valued_subset: