--- a/src/HOL/Relation.thy Fri Dec 07 14:29:09 2012 +0100
+++ b/src/HOL/Relation.thy Fri Dec 07 15:53:28 2012 +0100
@@ -919,7 +919,7 @@
subsubsection {* Image of a set under a relation *}
-definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixl "``" 90)
+definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90)
where
"r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
--- a/src/HOL/Rings.thy Fri Dec 07 14:29:09 2012 +0100
+++ b/src/HOL/Rings.thy Fri Dec 07 15:53:28 2012 +0100
@@ -95,7 +95,7 @@
class dvd = times
begin
-definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
+definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
"b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"