src/HOL/Library/Polynomial_GCD_euclidean.thy
2016-02-17 haftmann 2016-02-17 separated potentially conflicting type class instance into separate theory