src/HOL/Computational_Algebra/Field_as_Ring.thy
changeset 66817 0b12755ccbb2
parent 65435 378175f44328
child 66838 17989f6bc7b2
     1.1 --- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation real :: unique_euclidean_ring
     1.8 +instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
     1.9  begin
    1.10  
    1.11  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    1.12 @@ -55,7 +55,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -instantiation rat :: unique_euclidean_ring
    1.17 +instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
    1.18  begin
    1.19  
    1.20  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    1.21 @@ -86,7 +86,7 @@
    1.22  
    1.23  end
    1.24  
    1.25 -instantiation complex :: unique_euclidean_ring
    1.26 +instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
    1.27  begin
    1.28  
    1.29  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"