Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/GCD.thy
changeset 61649 268d88ec9087
parent 61605 1bf7b186542e
child 61799 4cf66f21b764 
--- a/src/HOL/GCD.thy	Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/GCD.thy	Fri Nov 13 12:27:13 2015 +0000
@@ -1133,10 +1133,7 @@
   apply (erule subst)
   apply (rule iffI)
   apply force
-  apply (drule_tac x = "abs e" for e in exI)
-  apply (case_tac "e >= 0" for e :: int)
-  apply force
-  apply force
+  using abs_dvd_iff abs_ge_zero apply blast
   done
 
 lemma gcd_coprime_nat:
isabelle