src/HOL/GCD.thy
changeset 68270 2bc921b2159b
parent 67399 eab6ce8368fa
child 68708 77858f347020
     1.1 --- a/src/HOL/GCD.thy	Thu May 24 22:28:26 2018 +0200
     1.2 +++ b/src/HOL/GCD.thy	Thu May 24 09:26:26 2018 +0000
     1.3 @@ -1287,7 +1287,7 @@
     1.4      by (simp add: t_def)
     1.5  qed
     1.6  
     1.7 -lemma gcd_eq_1_imp_coprime:
     1.8 +lemma gcd_eq_1_imp_coprime [dest!]:
     1.9    "coprime a b" if "gcd a b = 1"
    1.10  proof (rule coprimeI)
    1.11    fix c