corrected nonsensical associativity of `` and dvd
authornipkow
Fri Dec 07 15:53:28 2012 +0100 (2012-12-07)
changeset 50420f1a27e82af16
parent 50419 3177d0374701
child 50421 eb7b59cc8e08
corrected nonsensical associativity of `` and dvd
src/HOL/Relation.thy
src/HOL/Rings.thy
     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  
     2.1 --- a/src/HOL/Rings.thy	Fri Dec 07 14:29:09 2012 +0100
     2.2 +++ b/src/HOL/Rings.thy	Fri Dec 07 15:53:28 2012 +0100
     2.3 @@ -95,7 +95,7 @@
     2.4  class dvd = times
     2.5  begin
     2.6  
     2.7 -definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
     2.8 +definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
     2.9    "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
    2.10  
    2.11  lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"