--- a/src/HOL/Library/Nonpos_Ints.thy Tue Jan 05 21:55:40 2016 +0100
+++ b/src/HOL/Library/Nonpos_Ints.thy Tue Jan 05 21:57:21 2016 +0100
@@ -46,7 +46,7 @@
hence "(of_int m :: 'a) = of_nat n" by simp
also have "... = of_int (int n)" by simp
finally have "m = int n" by (subst (asm) of_int_eq_iff)
- with `m \<le> 0` show "n = 0" by auto
+ with \<open>m \<le> 0\<close> show "n = 0" by auto
qed simp
lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0"
@@ -84,10 +84,10 @@
proof
assume "of_real x \<in> (\<int>\<^sub>\<le>\<^sub>0 :: 'a set)"
then obtain n where "(of_real x :: 'a) = of_int n" "n \<le> 0" by (erule nonpos_Ints_cases)
- note `of_real x = of_int n`
+ note \<open>of_real x = of_int n\<close>
also have "of_int n = of_real (of_int n)" by (rule of_real_of_int_eq [symmetric])
finally have "x = of_int n" by (subst (asm) of_real_eq_iff)
- with `n \<le> 0` show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int)
+ with \<open>n \<le> 0\<close> show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int)
qed (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int)
lemma nonpos_Ints_altdef: "\<int>\<^sub>\<le>\<^sub>0 = {n \<in> \<int>. (n :: 'a :: linordered_idom) \<le> 0}"
--- a/src/HOL/Library/Poly_Deriv.thy Tue Jan 05 21:55:40 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy Tue Jan 05 21:57:21 2016 +0100
@@ -167,7 +167,7 @@
proof -
assume "p\<noteq>0"
then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
- have gt_0:"lead_coeff p >0" using pCons(3) `p\<noteq>0` by auto
+ have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
def n\<equiv>"max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
show ?thesis
proof (rule_tac x=n in exI,rule,rule)
@@ -176,9 +176,9 @@
using gte_lcoeff unfolding n_def by auto
hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
by (intro frac_le,auto)
- hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using `n\<le>x`[unfolded n_def] by auto
+ hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
- using `lead_coeff p \<le> poly p x` `poly p x>0` `p\<noteq>0`
+ using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
by (auto simp add:field_simps)
qed
qed
--- a/src/HOL/Library/Polynomial.thy Tue Jan 05 21:55:40 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy Tue Jan 05 21:57:21 2016 +0100
@@ -475,7 +475,7 @@
coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
by (simp add: field_simps setsum_right_distrib coeff_pCons)
also note setsum_atMost_Suc_shift[symmetric]
- also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]
+ also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
finally show ?thesis .
qed simp
qed simp
@@ -2145,19 +2145,19 @@
next
case False assume "degree (q * pcompose p q) = 0"
hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)
- moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) `p\<noteq>0`
+ moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) \<open>p\<noteq>0\<close>
proof -
assume "pcompose p q=0" "degree q\<noteq>0"
hence "degree p=0" using pCons.hyps(2) by auto
then obtain a1 where "p=[:a1:]"
by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
- thus False using `pcompose p q=0` `p\<noteq>0` by auto
+ thus False using \<open>pcompose p q=0\<close> \<open>p\<noteq>0\<close> by auto
qed
ultimately have "degree (pCons a p) * degree q=0" by auto
moreover have "degree (pcompose (pCons a p) q) = 0"
proof -
have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
- using `degree (q * pcompose p q) = 0` by simp
+ using \<open>degree (q * pcompose p q) = 0\<close> by simp
also have "... \<ge> degree ([:a:] + q * pcompose p q)"
by (rule degree_add_le_max)
finally show ?thesis by (auto simp add:pcompose_pCons)
@@ -2172,7 +2172,7 @@
unfolding pcompose_pCons
using degree_add_eq_right[of "[:a:]" ] asm by auto
thus ?thesis
- using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto
+ using pCons.hyps(2) degree_mult_eq[OF \<open>q\<noteq>0\<close> \<open>pcompose p q\<noteq>0\<close>] by auto
qed
ultimately show ?case by blast
qed
@@ -2186,11 +2186,11 @@
then obtain a where "p=[:a:]"
by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
hence "a=0" using assms(1) by auto
- thus ?thesis using `p=[:a:]` by simp
+ thus ?thesis using \<open>p=[:a:]\<close> by simp
qed
-subsection {* Leading coefficient *}
+subsection \<open>Leading coefficient\<close>
definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
"lead_coeff p= coeff p (degree p)"
@@ -2232,7 +2232,7 @@
proof -
assume "degree ( q * pcompose p q) = 0"
hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
- hence "p=0" using pcompose_eq_0[OF _ `degree q > 0`] by simp
+ hence "p=0" using pcompose_eq_0[OF _ \<open>degree q > 0\<close>] by simp
thus ?thesis by auto
qed
moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case"
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Tue Jan 05 21:55:40 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Tue Jan 05 21:57:21 2016 +0100
@@ -169,7 +169,7 @@
also have "\<dots> \<le> dist z (of_int n)"
using round_Re_minimises_norm[of z] by (simp add: dist_complex_def)
finally have "dist t (of_int n) > 0" by simp
- with `t = of_int n` show False by simp
+ with \<open>t = of_int n\<close> show False by simp
qed
lemma no_nonpos_Int_in_ball':
@@ -377,7 +377,7 @@
finally have "of_nat N \<ge> 2 * (norm z + d)" .
moreover have "N \<ge> 2" "N \<ge> M" unfolding N_def by simp_all
moreover have "(\<Sum>k=m..n. 1/(of_nat k)\<^sup>2) < e'" if "m \<ge> N" for m n
- using M[OF order.trans[OF `N \<ge> M` that]] unfolding real_norm_def
+ using M[OF order.trans[OF \<open>N \<ge> M\<close> that]] unfolding real_norm_def
by (subst (asm) abs_of_nonneg) (auto intro: setsum_nonneg simp: divide_simps)
moreover note calculation
} note N = this
@@ -1959,7 +1959,7 @@
let ?h = "\<lambda>z::complex. (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))"
def h \<equiv> "\<lambda>z::complex. if z \<in> \<int> then 0 else ?h z"
- -- \<open>@{term g} is periodic with period 1.\<close>
+ \<comment> \<open>@{term g} is periodic with period 1.\<close>
interpret g: periodic_fun_simple' g
proof
fix z :: complex
@@ -1979,7 +1979,7 @@
qed (simp add: g_def)
qed
- -- \<open>@{term g} is entire.\<close>
+ \<comment> \<open>@{term g} is entire.\<close>
have g_g': "(g has_field_derivative (h z * g z)) (at z)" for z :: complex
proof (cases "z \<in> \<int>")
let ?h' = "\<lambda>z. Beta z (1 - z) * ((Digamma z - Digamma (1 - z)) * sin (z * of_real pi) +
@@ -2204,7 +2204,7 @@
show ?thesis
proof (cases "z \<in> \<int>")
case False
- with `g z = pi` show ?thesis by (auto simp: g_def divide_simps)
+ with \<open>g z = pi\<close> show ?thesis by (auto simp: g_def divide_simps)
next
case True
then obtain n where n: "z = of_int n" by (elim Ints_cases)
--- a/src/HOL/Multivariate_Analysis/Summation.thy Tue Jan 05 21:55:40 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Summation.thy Tue Jan 05 21:57:21 2016 +0100
@@ -141,7 +141,7 @@
with l obtain l' where l': "l = ereal l'" by (cases l) simp_all
def c \<equiv> "(1 - l') / 2"
- from l and `l \<ge> 0` have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def
+ from l and \<open>l \<ge> 0\<close> have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def
by (simp_all add: field_simps l')
have "\<forall>C>l. eventually (\<lambda>n. ereal (root n (norm (f n))) < C) sequentially"
by (subst Limsup_le_iff[symmetric]) (simp add: l_def)