# HG changeset patch
# User haftmann
# Date 1240918485 -7200
# Node ID 41fd307cab30c11e88b21f6c1830bed03c32e04f
# Parent  b8f4e351b5bf3cb4b2ddf97b33b428c204d36d00
dropped reference to class recpower and lemma duplicate

diff -r b8f4e351b5bf -r 41fd307cab30 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Apr 27 19:44:30 2009 -0700
+++ b/src/HOL/Divides.thy	Tue Apr 28 13:34:45 2009 +0200
@@ -333,8 +333,9 @@
 
 end
 
-lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
-    (x div y)^n = x^n div y^n"
+lemma div_power:
+  "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
+    (x div y) ^ n = x ^ n div y ^ n"
 apply (induct n)
  apply simp
 apply(simp add: div_mult_div_if_dvd dvd_power_same)
@@ -936,10 +937,8 @@
 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
 
-lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
-  by (induct n) auto
-
-lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
+lemma power_dvd_imp_le:
+  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
   apply (rule power_le_imp_le_exp, assumption)
   apply (erule dvd_imp_le, simp)
   done