# HG changeset patch
# User wenzelm
# Date 1413817213 -7200
# Node ID 48395c763059279be5699db11431dd114f7d7e74
# Parent  50086388187469189b2c44a16452ba548c7a5a11
repared document;

diff -r 500863881874 -r 48395c763059 src/HOL/Parity.thy
--- 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