src/HOL/Relation.thy
changeset 12487 bbd564190c9b
parent 11136 e34e7f6d9b57
child 12905 bbbae3f359e6
     1.1 --- a/src/HOL/Relation.thy	Thu Dec 13 15:45:03 2001 +0100
     1.2 +++ b/src/HOL/Relation.thy	Thu Dec 13 16:47:35 2001 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
     1.5  
     1.6  constdefs
     1.7 -  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     1.8 +  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     1.9      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    1.10  
    1.11    Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)