src/HOL/Relation.thy
changeset 20716 a6686a8e1b68
parent 19656 09be06943252
child 21210 c17fd2df4e9e
     1.1 --- a/src/HOL/Relation.thy	Tue Sep 26 13:34:35 2006 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Sep 26 17:33:04 2006 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    converse  ("(_\<inverse>)" [1000] 999)
     1.5  
     1.6  definition
     1.7 -  rel_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" 75)
     1.9    "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
    1.10  
    1.11    Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)