--- a/src/HOL/Parity.thy Mon Oct 20 16:53:50 2014 +0200
+++ b/src/HOL/Parity.thy Mon Oct 20 17:00:13 2014 +0200
@@ -431,7 +431,7 @@
"odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
-lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. zero_le_power_eq\<close>
+lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
"0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
proof (cases "even n")
case True