src/HOL/GCD.thy
changeset 61649 268d88ec9087
parent 61605 1bf7b186542e
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/GCD.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -1133,10 +1133,7 @@
     1.4    apply (erule subst)
     1.5    apply (rule iffI)
     1.6    apply force
     1.7 -  apply (drule_tac x = "abs e" for e in exI)
     1.8 -  apply (case_tac "e >= 0" for e :: int)
     1.9 -  apply force
    1.10 -  apply force
    1.11 +  using abs_dvd_iff abs_ge_zero apply blast
    1.12    done
    1.13  
    1.14  lemma gcd_coprime_nat: