# HG changeset patch
# User haftmann
# Date 1332438879 -3600
# Node ID 08c22e8ffe70d0a6a9f040dcc62ecb23d2f67b18
# Parent  69276374c0a1f7a41baeefbcbd215dd742c2f75a
fixed typo

diff -r 69276374c0a1 -r 08c22e8ffe70 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Mar 22 18:37:20 2012 +0100
+++ b/src/HOL/Relation.thy	Thu Mar 22 18:54:39 2012 +0100
@@ -543,7 +543,7 @@
   "{} O R = {}"
   by blast
 
-lemma prod_comp_bot1 [simp]:
+lemma pred_comp_bot1 [simp]:
   "\<bottom> OO R = \<bottom>"
   by (fact rel_comp_empty1 [to_pred])