Added simp-rules: "R O {} = {}" and "{} O R = {}"

--- a/src/HOL/Relation.thy	Fri Jun 01 10:44:31 2007 +0200
+++ b/src/HOL/Relation.thy	Fri Jun 01 15:12:56 2007 +0200
@@ -147,6 +147,12 @@
 lemma Id_O_R [simp]: "Id O R = R"
   by fast
 
+lemma rel_comp_empty1[simp]: "{} O R = {}"
+  by blast
+
+lemma rel_comp_empty2[simp]: "R O {} = {}"
+  by blast
+
 lemma O_assoc: "(R O S) O T = R O (S O T)"
   by blast