# HG changeset patch
# User huffman
# Date 1245113976 25200
# Node ID 1e252b8b2334014df45840734fee63b1aa19e78e
# Parent  84912dff2d746d64a57c15e0bde315cefc30927a
move lemma div_power into semiring_div context; class ring_div inherits from idom

diff -r 84912dff2d74 -r 1e252b8b2334 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Jun 13 17:31:56 2009 -0700
+++ b/src/HOL/Divides.thy	Mon Jun 15 17:59:36 2009 -0700
@@ -331,17 +331,16 @@
   "(a * c) mod (b * c) = (a mod b) * c"
   using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
 
-end
-
 lemma div_power:
-  "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
-    (x div y) ^ n = x ^ n div y ^ n"
+  "y 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)
 done
 
-class ring_div = semiring_div + comm_ring_1
+end
+
+class ring_div = semiring_div + idom
 begin
 
 text {* Negation respects modular equivalence. *}