src/HOL/Rings.thy
changeset 50420 f1a27e82af16
parent 49962 a8cc904a6820
child 51520 e9b361845809
     1.1 --- a/src/HOL/Rings.thy	Fri Dec 07 14:29:09 2012 +0100
     1.2 +++ b/src/HOL/Rings.thy	Fri Dec 07 15:53:28 2012 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  class dvd = times
     1.5  begin
     1.6  
     1.7 -definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
     1.8 +definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
     1.9    "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
    1.10  
    1.11  lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"