fixed typo
authorhaftmann
Thu Mar 22 18:54:39 2012 +0100 (2012-03-22)
changeset 4708708c22e8ffe70
parent 47086 69276374c0a1
child 47088 eba1cea4eef6
fixed typo
src/HOL/Relation.thy
     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