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: