src/HOL/Computational_Algebra/Field_as_Ring.thy

--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Tue Jan 21 11:02:27 2020 +0100
@@ -24,7 +24,8 @@
 
 end
 
-instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instantiation real ::
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
@@ -55,7 +56,11 @@
 
 end
 
-instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance real :: field_gcd ..
+
+
+instantiation rat :: 
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
@@ -86,7 +91,11 @@
 
 end
 
-instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance rat :: field_gcd ..
+
+
+instantiation complex ::
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
@@ -117,4 +126,6 @@
 
 end
 
+instance complex :: field_gcd ..
+
 end