src/HOL/GCD.thy
changeset 44890 22f665a2e91c
parent 44845 5e51075cbd97
child 45264 3b2c770f6631
     1.1 --- a/src/HOL/GCD.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -525,7 +525,7 @@
     1.4  
     1.5  lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
     1.6  apply(rule antisym)
     1.7 - apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
     1.8 + apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
     1.9  apply simp
    1.10  done
    1.11  
    1.12 @@ -1604,7 +1604,7 @@
    1.13   apply simp
    1.14  apply (rule Max_le_iff[THEN iffD2])
    1.15    apply (metis all_not_in_conv finite_divisors_nat finite_INT)
    1.16 - apply fastsimp
    1.17 + apply fastforce
    1.18  apply clarsimp
    1.19  apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
    1.20  done
    1.21 @@ -1670,9 +1670,9 @@
    1.22           apply(rule Lcm_eq_Max_nat)
    1.23              apply simp
    1.24             apply blast
    1.25 -          apply fastsimp
    1.26 +          apply fastforce
    1.27           apply clarsimp
    1.28 -        apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
    1.29 +        apply(fastforce intro: finite_divisors_nat intro!: finite_INT)
    1.30          done
    1.31      qed
    1.32    qed