src/HOL/Relation.thy
changeset 57111 de33f3965ca6
parent 56790 f54097170704
child 58195 1fee63e0377d
     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: