| changeset 52392 | ee996ca08de3 |
| parent 50420 | f1a27e82af16 |
| child 52730 | 6bf02eb4ddf7 |
--- a/src/HOL/Relation.thy Tue Jun 18 15:52:47 2013 -0700 +++ b/src/HOL/Relation.thy Wed Jun 19 10:06:24 2013 +0200 @@ -416,6 +416,9 @@ "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" by (simp add: single_valued_def) +lemma simgle_valued_empty[simp]: "single_valued {}" +by(simp add: single_valued_def) + lemma single_valued_subset: "r \<subseteq> s ==> single_valued s ==> single_valued r" by (unfold single_valued_def) blast