src/HOL/Power.thy
 changeset 61799 4cf66f21b764 parent 61694 6571c78c9667 child 61944 5d06ecfdb472
```     1.1 --- a/src/HOL/Power.thy	Mon Dec 07 10:23:50 2015 +0100
1.2 +++ b/src/HOL/Power.thy	Mon Dec 07 10:38:04 2015 +0100
1.3 @@ -465,7 +465,7 @@
1.4    "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
1.5    by (induct n) auto
1.6
1.7 -text\<open>Surely we can strengthen this? It holds for @{text "0<a<1"} too.\<close>
1.8 +text\<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
1.9  lemma power_inject_exp [simp]:
1.10    "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
1.11    by (force simp add: order_antisym power_le_imp_le_exp)
1.12 @@ -482,7 +482,7 @@
1.13    by (induct n)
1.14     (auto simp add: mult_strict_mono le_less_trans [of 0 a b])
1.15
1.16 -text\<open>Lemma for @{text power_strict_decreasing}\<close>
1.17 +text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
1.18  lemma power_Suc_less:
1.19    "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
1.20    by (induct n)
1.21 @@ -501,7 +501,7 @@
1.22    done
1.23  qed
1.24
1.25 -text\<open>Proof resembles that of @{text power_strict_decreasing}\<close>
1.26 +text\<open>Proof resembles that of \<open>power_strict_decreasing\<close>\<close>
1.27  lemma power_decreasing [rule_format]:
1.28    "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n"
1.29  proof (induct N)
1.30 @@ -518,7 +518,7 @@
1.31    "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
1.32    using power_strict_decreasing [of 0 "Suc n" a] by simp
1.33
1.34 -text\<open>Proof again resembles that of @{text power_strict_decreasing}\<close>
1.35 +text\<open>Proof again resembles that of \<open>power_strict_decreasing\<close>\<close>
1.36  lemma power_increasing [rule_format]:
1.37    "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
1.38  proof (induct N)
1.39 @@ -531,7 +531,7 @@
1.40    done
1.41  qed
1.42
1.43 -text\<open>Lemma for @{text power_strict_increasing}\<close>
1.44 +text\<open>Lemma for \<open>power_strict_increasing\<close>\<close>
1.45  lemma power_less_power_Suc:
1.46    "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
1.47    by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one])
1.48 @@ -795,7 +795,7 @@
1.49    "Suc 0 ^ n = Suc 0"
1.50    by simp
1.51
1.52 -text\<open>Valid for the naturals, but what if @{text"0<i<1"}?
1.53 +text\<open>Valid for the naturals, but what if \<open>0<i<1\<close>?
1.54  Premises cannot be weakened: consider the case where @{term "i=0"},
1.55  @{term "m=1"} and @{term "n=0"}.\<close>
1.56  lemma nat_power_less_imp_less:
```