repared document;
authorwenzelm
Mon Oct 20 17:00:13 2014 +0200 (2014-10-20)
changeset 5871848395c763059
parent 58717 500863881874
child 58719 ac4f764c5be1
repared document;
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Mon Oct 20 16:53:50 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Mon Oct 20 17:00:13 2014 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
     1.5    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
     1.6  
     1.7 -lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. zero_le_power_eq\<close>
     1.8 +lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
     1.9    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
    1.10  proof (cases "even n")
    1.11    case True