--- 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])