# HG changeset patch
# User haftmann
# Date 1434138787 -7200
# Node ID b765e08f8bc067fb05aee3345f7bee4e1fdfa10c
# Parent  e1c345094813c4d445871ed8171f4ae9cf9dd6c0
proper subclass instances for existing gcd (semi)rings

diff -r e1c345094813 -r b765e08f8bc0 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- 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)