src/HOL/Relation.thy
changeset 47087 08c22e8ffe70
parent 46982 144d94446378
child 47375 8e6a45f1bf8f
child 47433 07f4bf913230
     1.1 --- a/src/HOL/Relation.thy	Thu Mar 22 18:37:20 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Thu Mar 22 18:54:39 2012 +0100
     1.3 @@ -543,7 +543,7 @@
     1.4    "{} O R = {}"
     1.5    by blast
     1.6  
     1.7 -lemma prod_comp_bot1 [simp]:
     1.8 +lemma pred_comp_bot1 [simp]:
     1.9    "\<bottom> OO R = \<bottom>"
    1.10    by (fact rel_comp_empty1 [to_pred])
    1.11