diff -r 627511c13164 -r dd8922885a68 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:20 2017 +0200
@@ -1510,21 +1510,6 @@
 lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
   by simp
 
-
-definition pairwise_coprime
-  where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
-
-lemma pairwise_coprimeI [intro?]:
-  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
-  by (simp add: pairwise_coprime_def)
-
-lemma pairwise_coprimeD:
-  "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
-  by (simp add: pairwise_coprime_def)
-
-lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
-  by (force simp: pairwise_coprime_def)
-
 end