# HG changeset patch
# User wenzelm
# Date 1185314128 -7200
# Node ID 9a18596359789f9117bc07f9e8f72e7ab72c9d60
# Parent  06f52a99fbd2ab8e4f76ec16527ae46d9a05cd22
fixed proofs involving dvd;

diff -r 06f52a99fbd2 -r 9a1859635978 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Tue Jul 24 22:59:53 2007 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Tue Jul 24 23:55:28 2007 +0200
@@ -51,9 +51,6 @@
 apply (rule_tac [2] disjI2)
 apply (erule_tac n = m in dvdE)
 apply (erule_tac [2] n = n in dvdE, auto)
-apply (rule_tac [2] k = p in dvd_mult_cancel)
-apply (rule_tac k = p in dvd_mult_cancel)
-apply (simp_all add: mult_ac)
 done
 
 
@@ -77,7 +74,6 @@
  apply (drule_tac x = nat in spec)
  apply (drule_tac x = b in spec)
  apply simp
- apply (blast intro: dvd_refl mult_dvd_mono)
 (*case 2: p dvd n*)
 apply (case_tac "b")
  apply simp
@@ -85,7 +81,6 @@
 apply (drule spec, drule spec, erule (1) notE impE)
 apply (drule_tac x = a in spec)
 apply (drule_tac x = nat in spec, simp)
-apply (blast intro: dvd_refl mult_dvd_mono)
 done
 
 (*needed in this form in Sylow.ML*)