Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Exponent.thy
changeset 31952 40501bb2d57c
parent 31717 d1f7b6245a75
child 32480 6c19da8e661a 
--- a/src/HOL/Algebra/Exponent.thy	Tue Jul 07 07:56:24 2009 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Tue Jul 07 17:39:51 2009 +0200
@@ -217,7 +217,7 @@
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)
   apply assumption
- prefer 2 apply (blast intro: nat_dvd_diff)
+ prefer 2 apply (blast intro: dvd_diff_nat)
 apply (drule gr0_implies_Suc, auto)
 done
 
@@ -233,7 +233,7 @@
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)
   apply assumption
- prefer 2 apply (blast intro: nat_dvd_diff)
+ prefer 2 apply (blast intro: dvd_diff_nat)
 apply (drule less_imp_Suc_add, auto)
 done
isabelle