# HG changeset patch
# User nipkow
# Date 1262360091 -3600
# Node ID 3ae38d4b090c6247de908a046282440f20b6fec7
# Parent  ada8eb23a08ea71836b0e6eff318ce1ba61ed10e
removed FIXME

diff -r ada8eb23a08e -r 3ae38d4b090c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Dec 31 23:47:09 2009 +0100
+++ b/src/HOL/GCD.thy	Fri Jan 01 16:34:51 2010 +0100
@@ -878,7 +878,6 @@
   ultimately show ?thesis by blast
 qed
 
-(* FIXME move to Divides(?) *)
 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   by (auto intro: pow_divides_pow_nat dvd_power_same)