--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy Sun Oct 08 22:28:22 2017 +0200
@@ -24,7 +24,7 @@
end
-instantiation real :: unique_euclidean_ring
+instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
begin
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
@@ -55,7 +55,7 @@
end
-instantiation rat :: unique_euclidean_ring
+instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
begin
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
@@ -86,7 +86,7 @@
end
-instantiation complex :: unique_euclidean_ring
+instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
begin
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"