# HG changeset patch
# User wenzelm
# Date 1434574879 -7200
# Node ID e0169291b31c23138a32f7a3078bfdd31e6dee84
# Parent  5e67a223a141e68b6522a354485b34d5fc23bfd6
tuned proofs -- slightly faster;

diff -r 5e67a223a141 -r e0169291b31c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jun 17 22:30:22 2015 +0200
+++ b/src/HOL/GCD.thy	Wed Jun 17 23:01:19 2015 +0200
@@ -525,9 +525,10 @@
 lemma finite_divisors_nat[simp]:
   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
 proof-
-  have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
+  have "finite{d. d <= m}"
+    by (blast intro: bounded_nat_set_is_finite)
   from finite_subset[OF _ this] show ?thesis using assms
-    by(bestsimp intro!:dvd_imp_le)
+    by (metis Collect_mono dvd_imp_le neq0_conv)
 qed
 
 lemma finite_divisors_int[simp]:
@@ -536,7 +537,7 @@
   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   hence "finite{d. abs d <= abs i}" by simp
   from finite_subset[OF _ this] show ?thesis using assms
-    by(bestsimp intro!:dvd_imp_le_int)
+    by (simp add: dvd_imp_le_int subset_iff)
 qed
 
 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"