changeset 56544 | b60d5d119489 |
parent 56536 | aefb4a8da31f |
child 57418 | 6ab1c7cb0b8d |
--- a/src/HOL/Power.thy Fri Apr 11 23:22:00 2014 +0200 +++ b/src/HOL/Power.thy Sat Apr 12 17:26:27 2014 +0200 @@ -297,7 +297,7 @@ lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n" - by (induct n) (simp_all add: mult_pos_pos) + by (induct n) simp_all lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"