src/HOL/Power.thy

--- a/src/HOL/Power.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Power.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -301,7 +301,7 @@
 
 lemma zero_le_power [simp]:
   "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
-  by (induct n) (simp_all add: mult_nonneg_nonneg)
+  by (induct n) simp_all
 
 lemma power_mono:
   "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"