src/HOL/Relation.thy
changeset 50420 f1a27e82af16
parent 48620 fc9be489e2fb
child 52392 ee996ca08de3
     1.1 --- a/src/HOL/Relation.thy	Fri Dec 07 14:29:09 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Dec 07 15:53:28 2012 +0100
     1.3 @@ -919,7 +919,7 @@
     1.4  
     1.5  subsubsection {* Image of a set under a relation *}
     1.6  
     1.7 -definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixl "``" 90)
     1.8 +definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90)
     1.9  where
    1.10    "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
    1.11