--- a/src/HOL/Power.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Power.thy Tue Dec 19 13:58:12 2017 +0100
@@ -651,7 +651,7 @@
lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
by (force simp add: power2_eq_square mult_less_0_iff)
-lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
+lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" \<comment> \<open>FIXME simp?\<close>
by (induct n) (simp_all add: abs_mult)
lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"