src/HOL/GCD.thy
changeset 59977 ad2d1cd53877
parent 59807 22bc39064290
child 60162 645058aa9d6f
     1.1 --- a/src/HOL/GCD.thy	Wed Apr 08 21:42:08 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Apr 08 21:48:59 2015 +0200
     1.3 @@ -49,8 +49,8 @@
     1.4  
     1.5  class semiring_gcd = comm_semiring_1 + gcd +
     1.6    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
     1.7 -		and gcd_dvd2 [iff]: "gcd a b dvd b"
     1.8 -		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
     1.9 +    and gcd_dvd2 [iff]: "gcd a b dvd b"
    1.10 +    and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    1.11  
    1.12  class ring_gcd = comm_ring_1 + semiring_gcd
    1.13