# HG changeset patch
# User wenzelm
# Date 1452027441 -3600
# Node ID bf3d9f1134748f22ee01ad17cb6d153759f883b8
# Parent  4e6e850e97c252f97798a16c1bae1fbc4ef1c128
isabelle update_cartouches -c -t;

diff -r 4e6e850e97c2 -r bf3d9f113474 src/HOL/Library/Nonpos_Ints.thy
--- 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}"
diff -r 4e6e850e97c2 -r bf3d9f113474 src/HOL/Library/Poly_Deriv.thy
--- 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
diff -r 4e6e850e97c2 -r bf3d9f113474 src/HOL/Library/Polynomial.thy
--- 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" 
diff -r 4e6e850e97c2 -r bf3d9f113474 src/HOL/Multivariate_Analysis/Gamma.thy
--- 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)
diff -r 4e6e850e97c2 -r bf3d9f113474 src/HOL/Multivariate_Analysis/Summation.thy
--- 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)