--- a/src/HOL/GCD.thy Thu May 24 22:28:26 2018 +0200
+++ b/src/HOL/GCD.thy Thu May 24 09:26:26 2018 +0000
@@ -1287,7 +1287,7 @@
by (simp add: t_def)
qed
-lemma gcd_eq_1_imp_coprime:
+lemma gcd_eq_1_imp_coprime [dest!]:
"coprime a b" if "gcd a b = 1"
proof (rule coprimeI)
fix c