diff -r 27f3c10b0b50 -r 4cf66f21b764 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Dec 07 10:23:50 2015 +0100 +++ b/src/HOL/Power.thy Mon Dec 07 10:38:04 2015 +0100 @@ -465,7 +465,7 @@ "of_nat x ^ n > 0 \ x > 0 \ n = 0" by (induct n) auto -text\Surely we can strengthen this? It holds for @{text "0 +text\Surely we can strengthen this? It holds for \0 too.\ lemma power_inject_exp [simp]: "1 < a \ a ^ m = a ^ n \ m = n" by (force simp add: order_antisym power_le_imp_le_exp) @@ -482,7 +482,7 @@ by (induct n) (auto simp add: mult_strict_mono le_less_trans [of 0 a b]) -text\Lemma for @{text power_strict_decreasing}\ +text\Lemma for \power_strict_decreasing\\ lemma power_Suc_less: "0 < a \ a < 1 \ a * a ^ n < a ^ n" by (induct n) @@ -501,7 +501,7 @@ done qed -text\Proof resembles that of @{text power_strict_decreasing}\ +text\Proof resembles that of \power_strict_decreasing\\ lemma power_decreasing [rule_format]: "n \ N \ 0 \ a \ a \ 1 \ a ^ N \ a ^ n" proof (induct N) @@ -518,7 +518,7 @@ "0 < a \ a < 1 \ a ^ Suc n < 1" using power_strict_decreasing [of 0 "Suc n" a] by simp -text\Proof again resembles that of @{text power_strict_decreasing}\ +text\Proof again resembles that of \power_strict_decreasing\\ lemma power_increasing [rule_format]: "n \ N \ 1 \ a \ a ^ n \ a ^ N" proof (induct N) @@ -531,7 +531,7 @@ done qed -text\Lemma for @{text power_strict_increasing}\ +text\Lemma for \power_strict_increasing\\ lemma power_less_power_Suc: "1 < a \ a ^ n < a * a ^ n" by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one]) @@ -795,7 +795,7 @@ "Suc 0 ^ n = Suc 0" by simp -text\Valid for the naturals, but what if @{text"0Valid for the naturals, but what if \0? Premises cannot be weakened: consider the case where @{term "i=0"}, @{term "m=1"} and @{term "n=0"}.\ lemma nat_power_less_imp_less: