src/HOL/GCD.thy
changeset 60512 e0169291b31c
parent 60357 bc0827281dc1
child 60580 7e741e22d7fc
     1.1 --- a/src/HOL/GCD.thy	Wed Jun 17 22:30:22 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Jun 17 23:01:19 2015 +0200
     1.3 @@ -525,9 +525,10 @@
     1.4  lemma finite_divisors_nat[simp]:
     1.5    assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
     1.6  proof-
     1.7 -  have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
     1.8 +  have "finite{d. d <= m}"
     1.9 +    by (blast intro: bounded_nat_set_is_finite)
    1.10    from finite_subset[OF _ this] show ?thesis using assms
    1.11 -    by(bestsimp intro!:dvd_imp_le)
    1.12 +    by (metis Collect_mono dvd_imp_le neq0_conv)
    1.13  qed
    1.14  
    1.15  lemma finite_divisors_int[simp]:
    1.16 @@ -536,7 +537,7 @@
    1.17    have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
    1.18    hence "finite{d. abs d <= abs i}" by simp
    1.19    from finite_subset[OF _ this] show ?thesis using assms
    1.20 -    by(bestsimp intro!:dvd_imp_le_int)
    1.21 +    by (simp add: dvd_imp_le_int subset_iff)
    1.22  qed
    1.23  
    1.24  lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"