src/HOL/GCD.thy
changeset 34221 3ae38d4b090c
parent 34030 829eb528b226
child 34222 e33ee7369ecb
     1.1 --- a/src/HOL/GCD.thy	Thu Dec 31 23:47:09 2009 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Jan 01 16:34:51 2010 +0100
     1.3 @@ -878,7 +878,6 @@
     1.4    ultimately show ?thesis by blast
     1.5  qed
     1.6  
     1.7 -(* FIXME move to Divides(?) *)
     1.8  lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
     1.9    by (auto intro: pow_divides_pow_nat dvd_power_same)
    1.10