Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed FIXME
authornipkow
Fri, 01 Jan 2010 16:34:51 +0100
changeset 34221 3ae38d4b090c
parent 34216 ada8eb23a08e
child 34222 e33ee7369ecb
removed FIXME
src/HOL/GCD.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle