--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 12 21:53:05 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 12 21:53:07 2015 +0200
@@ -1654,6 +1654,9 @@
lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
by (simp only: Gcd_insert Gcd_empty gcd_0) (cases "b = 0", simp, rule gcd_div_unit2, simp)
+subclass semiring_gcd
+ by unfold_locales (simp_all add: gcd_greatest_iff)
+
end
text {*
@@ -1668,6 +1671,8 @@
subclass euclidean_ring ..
+subclass ring_gcd ..
+
lemma gcd_neg1 [simp]:
"gcd (-a) b = gcd a b"
by (rule sym, rule gcdI, simp_all add: gcd_greatest)