# HG changeset patch
# User nipkow
# Date 1354892008 -3600
# Node ID f1a27e82af16f33a58b3c577de985ce0fe56efa0
# Parent  3177d03747010754baa15a7a770114143b3b7323
corrected nonsensical associativity of `` and dvd

diff -r 3177d0374701 -r f1a27e82af16 src/HOL/Relation.thy
--- 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}"
 
diff -r 3177d0374701 -r f1a27e82af16 src/HOL/Rings.thy
--- 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"