# HG changeset patch
# User wenzelm
# Date 1255619085 -7200
# Node ID 22664da2923b3494a87a9944c49064a15c015cb5
# Parent  63db9da65a1976cac1a432d715132d5686672d10
tuned proof (via atp_minimized);

diff -r 63db9da65a19 -r 22664da2923b src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Thu Oct 15 16:15:22 2009 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Thu Oct 15 17:04:45 2009 +0200
@@ -204,7 +204,7 @@
 apply (drule less_imp_le [of a])
 apply (drule le_imp_power_dvd)
 apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
-apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
+apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less nat_mult_commute not_add_less2 xt1(10))
 done
 
 lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]