--- a/src/HOL/GCD.thy Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/GCD.thy Sun Feb 15 17:01:22 2015 +0100
@@ -334,8 +334,7 @@
+ gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
apply default
apply (auto intro: dvd_antisym dvd_trans)[4]
-apply (metis dvd.dual_order.refl gcd_unique_nat)
-apply (auto intro: dvdI elim: dvdE)
+apply (metis dvd.dual_order.refl gcd_unique_nat)+
done
interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"