src/HOL/Computational_Algebra/Formal_Power_Series.thy
changeset 66817 0b12755ccbb2
parent 66806 a4e82b58d833
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -1425,6 +1425,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance fps :: (field) normalization_euclidean_semiring ..
     1.8 +
     1.9  instantiation fps :: (field) euclidean_ring_gcd
    1.10  begin
    1.11  definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"