src/HOL/Relation.thy
changeset 52392 ee996ca08de3
parent 50420 f1a27e82af16
child 52730 6bf02eb4ddf7
     1.1 --- a/src/HOL/Relation.thy	Tue Jun 18 15:52:47 2013 -0700
     1.2 +++ b/src/HOL/Relation.thy	Wed Jun 19 10:06:24 2013 +0200
     1.3 @@ -416,6 +416,9 @@
     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 +by(simp add: single_valued_def)
     1.9 +
    1.10  lemma single_valued_subset:
    1.11    "r \<subseteq> s ==> single_valued s ==> single_valued r"
    1.12    by (unfold single_valued_def) blast