# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1456690811 -3600
# Node ID 9590972c2caf2fe8a91385b7891779136b8e9012
# Parent  a3c7bd201da7b9b583d37f0db0a942254f7f9ea6# Parent  11e06f5283bc441589a730b053ebc0d4fb20c8cf
Merged

diff -r 11e06f5283bc -r 9590972c2caf src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Feb 28 19:56:57 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Feb 28 21:20:11 2016 +0100
@@ -234,6 +234,8 @@
 class euclidean_ring = euclidean_semiring + idom
 begin
 
+subclass ring_div ..
+
 function euclid_ext_aux :: "'a \<Rightarrow> _" where
   "euclid_ext_aux r' r s' s t' t = (
      if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r')
@@ -305,6 +307,10 @@
   "case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y"
   unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all
 
+lemma euclid_ext_gcd_eucl:
+  "(case euclid_ext x y of (a,b,c) \<Rightarrow> c) = gcd_eucl x y"
+  using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold)
+
 definition euclid_ext' where
   "euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))"