src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 60439 b765e08f8bc0
parent 60438 e1c345094813
child 60516 0826b7025d07
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:53:05 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:53:07 2015 +0200
     1.3 @@ -1654,6 +1654,9 @@
     1.4  lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
     1.5    by (simp only: Gcd_insert Gcd_empty gcd_0) (cases "b = 0", simp, rule gcd_div_unit2, simp)
     1.6  
     1.7 +subclass semiring_gcd
     1.8 +  by unfold_locales (simp_all add: gcd_greatest_iff)
     1.9 +  
    1.10  end
    1.11  
    1.12  text {*
    1.13 @@ -1668,6 +1671,8 @@
    1.14  
    1.15  subclass euclidean_ring ..
    1.16  
    1.17 +subclass ring_gcd ..
    1.18 +
    1.19  lemma gcd_neg1 [simp]:
    1.20    "gcd (-a) b = gcd a b"
    1.21    by (rule sym, rule gcdI, simp_all add: gcd_greatest)