# HG changeset patch
# User krauss
# Date 1180703576 -7200
# Node ID 1fa87978cf27f22ec837265c056b481e4163ecb6
# Parent  f3b967273975986e1f76ca4298164c4289fd7062
Added simp-rules: "R O {} = {}" and "{} O R = {}"

diff -r f3b967273975 -r 1fa87978cf27 src/HOL/Relation.thy
--- 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