isabelle update_cartouches;
authorwenzelm
Sat Jun 20 16:31:44 2015 +0200 (2015-06-20)
changeset 605331e7ccd864b62
parent 60532 7fb5b7dc8332
child 60534 b2add2b08412
isabelle update_cartouches;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Jun 20 16:23:56 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Jun 20 16:31:44 2015 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4   (* Author:     Johannes Hoelzl, TU Muenchen
     1.5     Coercions removed by Dmitriy Traytel *)
     1.6  
     1.7 -section {* Prove Real Valued Inequalities by Computation *}
     1.8 +section \<open>Prove Real Valued Inequalities by Computation\<close>
     1.9  
    1.10  theory Approximation
    1.11  imports
    1.12 @@ -18,7 +18,7 @@
    1.13  
    1.14  section "Horner Scheme"
    1.15  
    1.16 -subsection {* Define auxiliary helper @{text horner} function *}
    1.17 +subsection \<open>Define auxiliary helper @{text horner} function\<close>
    1.18  
    1.19  primrec horner :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> real" where
    1.20  "horner F G 0 i k x       = 0" |
    1.21 @@ -69,7 +69,7 @@
    1.22  next
    1.23    case (Suc n)
    1.24    thus ?case using lapprox_rat[of prec 1 "f j'"] using rapprox_rat[of 1 "f j'" prec]
    1.25 -    Suc[where j'="Suc j'"] `0 \<le> real x`
    1.26 +    Suc[where j'="Suc j'"] \<open>0 \<le> real x\<close>
    1.27      by (auto intro!: add_mono mult_left_mono float_round_down_le float_round_up_le
    1.28        order_trans[OF add_mono[OF _ float_plus_down_le]]
    1.29        order_trans[OF _ add_mono[OF _ float_plus_up_le]]
    1.30 @@ -78,12 +78,12 @@
    1.31  
    1.32  subsection "Theorems for floating point functions implementing the horner scheme"
    1.33  
    1.34 -text {*
    1.35 +text \<open>
    1.36  
    1.37  Here @{term_type "f :: nat \<Rightarrow> nat"} is the sequence defining the Taylor series, the coefficients are
    1.38  all alternating and reciprocs. We use @{term G} and @{term F} to describe the computation of @{term f}.
    1.39  
    1.40 -*}
    1.41 +\<close>
    1.42  
    1.43  lemma horner_bounds:
    1.44    fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.45 @@ -102,7 +102,7 @@
    1.46        (is "?ub")
    1.47  proof -
    1.48    have "?lb  \<and> ?ub"
    1.49 -    using horner_bounds'[where lb=lb, OF `0 \<le> real x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
    1.50 +    using horner_bounds'[where lb=lb, OF \<open>0 \<le> real x\<close> f_Suc lb_0 lb_Suc ub_0 ub_Suc]
    1.51      unfolding horner_schema[where f=f, OF f_Suc] .
    1.52    thus "?lb" and "?ub" by auto
    1.53  qed
    1.54 @@ -134,14 +134,14 @@
    1.55      by (auto simp: minus_float_round_up_eq minus_float_round_down_eq)
    1.56  qed
    1.57  
    1.58 -subsection {* Selectors for next even or odd number *}
    1.59 -
    1.60 -text {*
    1.61 +subsection \<open>Selectors for next even or odd number\<close>
    1.62 +
    1.63 +text \<open>
    1.64  
    1.65  The horner scheme computes alternating series. To get the upper and lower bounds we need to
    1.66  guarantee to access a even or odd member. To do this we use @{term get_odd} and @{term get_even}.
    1.67  
    1.68 -*}
    1.69 +\<close>
    1.70  
    1.71  definition get_odd :: "nat \<Rightarrow> nat" where
    1.72    "get_odd n = (if odd n then n else (Suc n))"
    1.73 @@ -189,12 +189,12 @@
    1.74  
    1.75  section "Square root"
    1.76  
    1.77 -text {*
    1.78 +text \<open>
    1.79  
    1.80  The square root computation is implemented as newton iteration. As first first step we use the
    1.81  nearest power of two greater than the square root.
    1.82  
    1.83 -*}
    1.84 +\<close>
    1.85  
    1.86  fun sqrt_iteration :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
    1.87  "sqrt_iteration prec 0 x = Float 1 ((bitlen \<bar>mantissa x\<bar> + exponent x) div 2 + 1)" |
    1.88 @@ -252,7 +252,7 @@
    1.89        unfolding Float by (auto simp: powr_realpow[symmetric] field_simps powr_add)
    1.90      also have "\<dots> < 1 * 2 powr (e + nat (bitlen m))"
    1.91      proof (rule mult_strict_right_mono, auto)
    1.92 -      show "m < 2^nat (bitlen m)" using bitlen_bounds[OF `0 < m`, THEN conjunct2]
    1.93 +      show "m < 2^nat (bitlen m)" using bitlen_bounds[OF \<open>0 < m\<close>, THEN conjunct2]
    1.94          unfolding real_of_int_less_iff[of m, symmetric] by auto
    1.95      qed
    1.96      finally have "sqrt x < sqrt (2 powr (e + bitlen m))" unfolding int_nat_bl by auto
    1.97 @@ -268,7 +268,7 @@
    1.98          have "?E mod 2 < 2" by auto
    1.99          from this[THEN zless_imp_add1_zle]
   1.100          have "?E mod 2 \<le> 0" using False by auto
   1.101 -        from xt1(5)[OF `0 \<le> ?E mod 2` this]
   1.102 +        from xt1(5)[OF \<open>0 \<le> ?E mod 2\<close> this]
   1.103          show ?thesis by auto
   1.104        qed
   1.105        hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)"
   1.106 @@ -286,16 +286,16 @@
   1.107          by simp
   1.108        finally show ?thesis by auto
   1.109      qed
   1.110 -    finally show ?thesis using `0 < m`
   1.111 +    finally show ?thesis using \<open>0 < m\<close>
   1.112        unfolding Float
   1.113        by (subst compute_sqrt_iteration_base) (simp add: ac_simps)
   1.114    qed
   1.115  next
   1.116    case (Suc n)
   1.117    let ?b = "sqrt_iteration prec n x"
   1.118 -  have "0 < sqrt x" using `0 < real x` by auto
   1.119 +  have "0 < sqrt x" using \<open>0 < real x\<close> by auto
   1.120    also have "\<dots> < real ?b" using Suc .
   1.121 -  finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
   1.122 +  finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ \<open>0 < real x\<close>] by auto
   1.123    also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2"
   1.124      by (rule divide_right_mono, auto simp add: float_divr)
   1.125    also have "\<dots> = (Float 1 (- 1)) * (?b + (float_divr prec x ?b))" by simp
   1.126 @@ -315,12 +315,12 @@
   1.127  lemma lb_sqrt_lower_bound: assumes "0 \<le> real x"
   1.128    shows "0 \<le> real (lb_sqrt prec x)"
   1.129  proof (cases "0 < x")
   1.130 -  case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` by auto
   1.131 +  case True hence "0 < real x" and "0 \<le> x" using \<open>0 \<le> real x\<close> by auto
   1.132    hence "0 < sqrt_iteration prec prec x" using sqrt_iteration_lower_bound by auto
   1.133 -  hence "0 \<le> real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \<le> x`] unfolding less_eq_float_def by auto
   1.134 +  hence "0 \<le> real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF \<open>0 \<le> x\<close>] unfolding less_eq_float_def by auto
   1.135    thus ?thesis unfolding lb_sqrt.simps using True by auto
   1.136  next
   1.137 -  case False with `0 \<le> real x` have "real x = 0" by auto
   1.138 +  case False with \<open>0 \<le> real x\<close> have "real x = 0" by auto
   1.139    thus ?thesis unfolding lb_sqrt.simps by auto
   1.140  qed
   1.141  
   1.142 @@ -334,13 +334,13 @@
   1.143      have "(float_divl prec x (sqrt_iteration prec prec x)) \<le>
   1.144            x / (sqrt_iteration prec prec x)" by (rule float_divl)
   1.145      also have "\<dots> < x / sqrt x"
   1.146 -      by (rule divide_strict_left_mono[OF sqrt_ub `0 < real x`
   1.147 +      by (rule divide_strict_left_mono[OF sqrt_ub \<open>0 < real x\<close>
   1.148                 mult_pos_pos[OF order_less_trans[OF sqrt_gt0 sqrt_ub] sqrt_gt0]])
   1.149      also have "\<dots> = sqrt x"
   1.150        unfolding inverse_eq_iff_eq[of _ "sqrt x", symmetric]
   1.151 -                sqrt_divide_self_eq[OF `0 \<le> real x`, symmetric] by auto
   1.152 +                sqrt_divide_self_eq[OF \<open>0 \<le> real x\<close>, symmetric] by auto
   1.153      finally have "lb_sqrt prec x \<le> sqrt x"
   1.154 -      unfolding lb_sqrt.simps if_P[OF `0 < x`] by auto }
   1.155 +      unfolding lb_sqrt.simps if_P[OF \<open>0 < x\<close>] by auto }
   1.156    note lb = this
   1.157  
   1.158    { fix x :: float assume "0 < x"
   1.159 @@ -349,7 +349,7 @@
   1.160      hence "sqrt x < sqrt_iteration prec prec x"
   1.161        using sqrt_iteration_bound by auto
   1.162      hence "sqrt x \<le> ub_sqrt prec x"
   1.163 -      unfolding ub_sqrt.simps if_P[OF `0 < x`] by auto }
   1.164 +      unfolding ub_sqrt.simps if_P[OF \<open>0 < x\<close>] by auto }
   1.165    note ub = this
   1.166  
   1.167    show ?thesis
   1.168 @@ -377,12 +377,12 @@
   1.169  
   1.170  subsection "Compute arcus tangens series"
   1.171  
   1.172 -text {*
   1.173 +text \<open>
   1.174  
   1.175  As first step we implement the computation of the arcus tangens series. This is only valid in the range
   1.176  @{term "{-1 :: real .. 1}"}. This is used to compute \<pi> and then the entire arcus tangens.
   1.177  
   1.178 -*}
   1.179 +\<close>
   1.180  
   1.181  fun ub_arctan_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
   1.182  and lb_arctan_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
   1.183 @@ -403,18 +403,18 @@
   1.184  
   1.185    have "0 \<le> sqrt y" using assms by auto
   1.186    have "sqrt y \<le> 1" using assms by auto
   1.187 -  from `even n` obtain m where "2 * m = n" by (blast elim: evenE)
   1.188 +  from \<open>even n\<close> obtain m where "2 * m = n" by (blast elim: evenE)
   1.189  
   1.190    have "arctan (sqrt y) \<in> { ?S n .. ?S (Suc n) }"
   1.191    proof (cases "sqrt y = 0")
   1.192      case False
   1.193 -    hence "0 < sqrt y" using `0 \<le> sqrt y` by auto
   1.194 +    hence "0 < sqrt y" using \<open>0 \<le> sqrt y\<close> by auto
   1.195      hence prem: "0 < 1 / (0 * 2 + (1::nat)) * sqrt y ^ (0 * 2 + 1)" by auto
   1.196  
   1.197 -    have "\<bar> sqrt y \<bar> \<le> 1"  using `0 \<le> sqrt y` `sqrt y \<le> 1` by auto
   1.198 +    have "\<bar> sqrt y \<bar> \<le> 1"  using \<open>0 \<le> sqrt y\<close> \<open>sqrt y \<le> 1\<close> by auto
   1.199      from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this]
   1.200 -      monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`]
   1.201 -    show ?thesis unfolding arctan_series[OF `\<bar> sqrt y \<bar> \<le> 1`] Suc_eq_plus1 atLeast0LessThan .
   1.202 +      monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded \<open>2 * m = n\<close>]
   1.203 +    show ?thesis unfolding arctan_series[OF \<open>\<bar> sqrt y \<bar> \<le> 1\<close>] Suc_eq_plus1 atLeast0LessThan .
   1.204    qed auto
   1.205    note arctan_bounds = this[unfolded atLeastAtMost_iff]
   1.206  
   1.207 @@ -423,10 +423,10 @@
   1.208    note bounds = horner_bounds[where s=1 and f="\<lambda>i. 2 * i + 1" and j'=0
   1.209      and lb="\<lambda>n i k x. lb_arctan_horner prec n k x"
   1.210      and ub="\<lambda>n i k x. ub_arctan_horner prec n k x",
   1.211 -    OF `0 \<le> real y` F lb_arctan_horner.simps ub_arctan_horner.simps]
   1.212 +    OF \<open>0 \<le> real y\<close> F lb_arctan_horner.simps ub_arctan_horner.simps]
   1.213  
   1.214    { have "(sqrt y * lb_arctan_horner prec n 1 y) \<le> ?S n"
   1.215 -      using bounds(1) `0 \<le> sqrt y`
   1.216 +      using bounds(1) \<open>0 \<le> sqrt y\<close>
   1.217        unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
   1.218        unfolding mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult
   1.219        by (auto intro!: mult_left_mono)
   1.220 @@ -435,7 +435,7 @@
   1.221    moreover
   1.222    { have "arctan (sqrt y) \<le> ?S (Suc n)" using arctan_bounds ..
   1.223      also have "\<dots> \<le> (sqrt y * ub_arctan_horner prec (Suc n) 1 y)"
   1.224 -      using bounds(2)[of "Suc n"] `0 \<le> sqrt y`
   1.225 +      using bounds(2)[of "Suc n"] \<open>0 \<le> sqrt y\<close>
   1.226        unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
   1.227        unfolding mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult
   1.228        by (auto intro!: mult_left_mono)
   1.229 @@ -479,8 +479,8 @@
   1.230  proof cases
   1.231    assume "x \<noteq> 0"
   1.232    with assms have "z \<le> arctan y / y" by (simp add: field_simps)
   1.233 -  also have "\<dots> \<le> arctan x / x" using assms `x \<noteq> 0` by (auto intro!: arctan_divide_mono)
   1.234 -  finally show ?thesis using assms `x \<noteq> 0` by (simp add: field_simps)
   1.235 +  also have "\<dots> \<le> arctan x / x" using assms \<open>x \<noteq> 0\<close> by (auto intro!: arctan_divide_mono)
   1.236 +  finally show ?thesis using assms \<open>x \<noteq> 0\<close> by (simp add: field_simps)
   1.237  qed simp
   1.238  
   1.239  lemma arctan_le_mult:
   1.240 @@ -500,16 +500,16 @@
   1.241    from assms have "real xl \<le> 1" "sqrt (real xl) \<le> x" "x \<le> sqrt (real xu)" "0 \<le> real xu"
   1.242      "0 \<le> real xl" "0 < sqrt (real xl)"
   1.243      by (auto intro!: real_le_rsqrt real_le_lsqrt simp: power2_eq_square)
   1.244 -  from arctan_0_1_bounds[OF `0 \<le> real xu`  `real xu \<le> 1`]
   1.245 +  from arctan_0_1_bounds[OF \<open>0 \<le> real xu\<close>  \<open>real xu \<le> 1\<close>]
   1.246    have "sqrt (real xu) * real (lb_arctan_horner p1 (get_even n) 1 xu) \<le> arctan (sqrt (real xu))"
   1.247      by simp
   1.248 -  from arctan_mult_le[OF `0 \<le> x` `x \<le> sqrt _`  this]
   1.249 +  from arctan_mult_le[OF \<open>0 \<le> x\<close> \<open>x \<le> sqrt _\<close>  this]
   1.250    have "x * real (lb_arctan_horner p1 (get_even n) 1 xu) \<le> arctan x" .
   1.251    moreover
   1.252 -  from arctan_0_1_bounds[OF `0 \<le> real xl`  `real xl \<le> 1`]
   1.253 +  from arctan_0_1_bounds[OF \<open>0 \<le> real xl\<close>  \<open>real xl \<le> 1\<close>]
   1.254    have "arctan (sqrt (real xl)) \<le> sqrt (real xl) * real (ub_arctan_horner p2 (get_odd n) 1 xl)"
   1.255      by simp
   1.256 -  from arctan_le_mult[OF `0 < sqrt xl` `sqrt xl \<le> x` this]
   1.257 +  from arctan_le_mult[OF \<open>0 < sqrt xl\<close> \<open>sqrt xl \<le> x\<close> this]
   1.258    have "arctan x \<le> x * real (ub_arctan_horner p2 (get_odd n) 1 xl)" .
   1.259    ultimately show ?thesis by simp
   1.260  qed
   1.261 @@ -567,16 +567,16 @@
   1.262    { fix prec n :: nat fix k :: int assume "1 < k" hence "0 \<le> k" and "0 < k" and "1 \<le> k" by auto
   1.263      let ?k = "rapprox_rat prec 1 k"
   1.264      let ?kl = "float_round_down (Suc prec) (?k * ?k)"
   1.265 -    have "1 div k = 0" using div_pos_pos_trivial[OF _ `1 < k`] by auto
   1.266 -
   1.267 -    have "0 \<le> real ?k" by (rule order_trans[OF _ rapprox_rat]) (auto simp add: `0 \<le> k`)
   1.268 +    have "1 div k = 0" using div_pos_pos_trivial[OF _ \<open>1 < k\<close>] by auto
   1.269 +
   1.270 +    have "0 \<le> real ?k" by (rule order_trans[OF _ rapprox_rat]) (auto simp add: \<open>0 \<le> k\<close>)
   1.271      have "real ?k \<le> 1"
   1.272 -      by (auto simp add: `0 < k` `1 \<le> k` less_imp_le
   1.273 +      by (auto simp add: \<open>0 < k\<close> \<open>1 \<le> k\<close> less_imp_le
   1.274          intro!: mult_nonneg_le_one order_trans[OF _ rapprox_rat] rapprox_rat_le1)
   1.275      have "1 / k \<le> ?k" using rapprox_rat[where x=1 and y=k] by auto
   1.276      hence "arctan (1 / k) \<le> arctan ?k" by (rule arctan_monotone')
   1.277      also have "\<dots> \<le> (?k * ub_arctan_horner prec (get_odd n) 1 ?kl)"
   1.278 -      using arctan_0_1_bounds_round[OF `0 \<le> real ?k` `real ?k \<le> 1`]
   1.279 +      using arctan_0_1_bounds_round[OF \<open>0 \<le> real ?k\<close> \<open>real ?k \<le> 1\<close>]
   1.280        by auto
   1.281      finally have "arctan (1 / k) \<le> ?k * ub_arctan_horner prec (get_odd n) 1 ?kl" .
   1.282    } note ub_arctan = this
   1.283 @@ -584,20 +584,20 @@
   1.284    { fix prec n :: nat fix k :: int assume "1 < k" hence "0 \<le> k" and "0 < k" by auto
   1.285      let ?k = "lapprox_rat prec 1 k"
   1.286      let ?ku = "float_round_up (Suc prec) (?k * ?k)"
   1.287 -    have "1 div k = 0" using div_pos_pos_trivial[OF _ `1 < k`] by auto
   1.288 -    have "1 / k \<le> 1" using `1 < k` by auto
   1.289 -    have "0 \<le> real ?k" using lapprox_rat_nonneg[where x=1 and y=k, OF zero_le_one `0 \<le> k`]
   1.290 -      by (auto simp add: `1 div k = 0`)
   1.291 +    have "1 div k = 0" using div_pos_pos_trivial[OF _ \<open>1 < k\<close>] by auto
   1.292 +    have "1 / k \<le> 1" using \<open>1 < k\<close> by auto
   1.293 +    have "0 \<le> real ?k" using lapprox_rat_nonneg[where x=1 and y=k, OF zero_le_one \<open>0 \<le> k\<close>]
   1.294 +      by (auto simp add: \<open>1 div k = 0\<close>)
   1.295      have "0 \<le> real (?k * ?k)" by simp
   1.296 -    have "real ?k \<le> 1" using lapprox_rat by (rule order_trans, auto simp add: `1 / k \<le> 1`)
   1.297 -    hence "real (?k * ?k) \<le> 1" using `0 \<le> real ?k` by (auto intro!: mult_nonneg_le_one)
   1.298 +    have "real ?k \<le> 1" using lapprox_rat by (rule order_trans, auto simp add: \<open>1 / k \<le> 1\<close>)
   1.299 +    hence "real (?k * ?k) \<le> 1" using \<open>0 \<le> real ?k\<close> by (auto intro!: mult_nonneg_le_one)
   1.300  
   1.301      have "?k \<le> 1 / k" using lapprox_rat[where x=1 and y=k] by auto
   1.302  
   1.303      have "?k * lb_arctan_horner prec (get_even n) 1 ?ku \<le> arctan ?k"
   1.304 -      using arctan_0_1_bounds_round[OF `0 \<le> real ?k` `real ?k \<le> 1`]
   1.305 +      using arctan_0_1_bounds_round[OF \<open>0 \<le> real ?k\<close> \<open>real ?k \<le> 1\<close>]
   1.306        by auto
   1.307 -    also have "\<dots> \<le> arctan (1 / k)" using `?k \<le> 1 / k` by (rule arctan_monotone')
   1.308 +    also have "\<dots> \<le> arctan (1 / k)" using \<open>?k \<le> 1 / k\<close> by (rule arctan_monotone')
   1.309      finally have "?k * lb_arctan_horner prec (get_even n) 1 ?ku \<le> arctan (1 / k)" .
   1.310    } note lb_arctan = this
   1.311  
   1.312 @@ -665,7 +665,7 @@
   1.313    shows "lb_arctan prec x \<le> arctan x"
   1.314  proof -
   1.315    have "\<not> x < 0" and "0 \<le> x"
   1.316 -    using `0 \<le> real x` by (auto intro!: truncate_up_le )
   1.317 +    using \<open>0 \<le> real x\<close> by (auto intro!: truncate_up_le )
   1.318  
   1.319    let "?ub_horner x" =
   1.320        "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (float_round_down (Suc prec) (x * x))"
   1.321 @@ -675,9 +675,9 @@
   1.322    show ?thesis
   1.323    proof (cases "x \<le> Float 1 (- 1)")
   1.324      case True hence "real x \<le> 1" by simp
   1.325 -    from arctan_0_1_bounds_round[OF `0 \<le> real x` `real x \<le> 1`]
   1.326 +    from arctan_0_1_bounds_round[OF \<open>0 \<le> real x\<close> \<open>real x \<le> 1\<close>]
   1.327      show ?thesis
   1.328 -      unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True] using `0 \<le> x`
   1.329 +      unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_P[OF True] using \<open>0 \<le> x\<close>
   1.330        by (auto intro!: float_round_down_le)
   1.331    next
   1.332      case False hence "0 < real x" by auto
   1.333 @@ -695,12 +695,12 @@
   1.334      finally
   1.335      have "sqrt (1 + x*x) \<le> ub_sqrt prec ?sxx" .
   1.336      hence "?R \<le> ?fR" by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le)
   1.337 -    hence "0 < ?fR" and "0 < real ?fR" using `0 < ?R` by auto
   1.338 +    hence "0 < ?fR" and "0 < real ?fR" using \<open>0 < ?R\<close> by auto
   1.339  
   1.340      have monotone: "?DIV \<le> x / ?R"
   1.341      proof -
   1.342        have "?DIV \<le> real x / ?fR" by (rule float_divl)
   1.343 -      also have "\<dots> \<le> x / ?R" by (rule divide_left_mono[OF `?R \<le> ?fR` `0 \<le> real x` mult_pos_pos[OF order_less_le_trans[OF divisor_gt0 `?R \<le> real ?fR`] divisor_gt0]])
   1.344 +      also have "\<dots> \<le> x / ?R" by (rule divide_left_mono[OF \<open>?R \<le> ?fR\<close> \<open>0 \<le> real x\<close> mult_pos_pos[OF order_less_le_trans[OF divisor_gt0 \<open>?R \<le> real ?fR\<close>] divisor_gt0]])
   1.345        finally show ?thesis .
   1.346      qed
   1.347  
   1.348 @@ -709,19 +709,19 @@
   1.349        case True
   1.350  
   1.351        have "x \<le> sqrt (1 + x * x)" using real_sqrt_sum_squares_ge2[where x=1, unfolded numeral_2_eq_2] by auto
   1.352 -      also note `\<dots> \<le> (ub_sqrt prec ?sxx)`
   1.353 +      also note \<open>\<dots> \<le> (ub_sqrt prec ?sxx)\<close>
   1.354        finally have "real x \<le> ?fR" by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le)
   1.355        moreover have "?DIV \<le> real x / ?fR" by (rule float_divl)
   1.356 -      ultimately have "real ?DIV \<le> 1" unfolding divide_le_eq_1_pos[OF `0 < real ?fR`, symmetric] by auto
   1.357 -
   1.358 -      have "0 \<le> real ?DIV" using float_divl_lower_bound[OF `0 \<le> x`] `0 < ?fR` unfolding less_eq_float_def by auto
   1.359 -
   1.360 -      from arctan_0_1_bounds_round[OF `0 \<le> real (?DIV)` `real (?DIV) \<le> 1`]
   1.361 +      ultimately have "real ?DIV \<le> 1" unfolding divide_le_eq_1_pos[OF \<open>0 < real ?fR\<close>, symmetric] by auto
   1.362 +
   1.363 +      have "0 \<le> real ?DIV" using float_divl_lower_bound[OF \<open>0 \<le> x\<close>] \<open>0 < ?fR\<close> unfolding less_eq_float_def by auto
   1.364 +
   1.365 +      from arctan_0_1_bounds_round[OF \<open>0 \<le> real (?DIV)\<close> \<open>real (?DIV) \<le> 1\<close>]
   1.366        have "Float 1 1 * ?lb_horner ?DIV \<le> 2 * arctan ?DIV" by simp
   1.367        also have "\<dots> \<le> 2 * arctan (x / ?R)"
   1.368          using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono arctan_monotone')
   1.369        also have "2 * arctan (x / ?R) = arctan x" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
   1.370 -      finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF True]
   1.371 +      finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 (- 1)\<close>] if_P[OF True]
   1.372          by (auto simp: float_round_down.rep_eq intro!: order_trans[OF mult_left_mono[OF truncate_down]])
   1.373      next
   1.374        case False
   1.375 @@ -729,32 +729,32 @@
   1.376        hence "1 \<le> real x" by auto
   1.377  
   1.378        let "?invx" = "float_divr prec 1 x"
   1.379 -      have "0 \<le> arctan x" using arctan_monotone'[OF `0 \<le> real x`] using arctan_tan[of 0, unfolded tan_zero] by auto
   1.380 +      have "0 \<le> arctan x" using arctan_monotone'[OF \<open>0 \<le> real x\<close>] using arctan_tan[of 0, unfolded tan_zero] by auto
   1.381  
   1.382        show ?thesis
   1.383        proof (cases "1 < ?invx")
   1.384          case True
   1.385 -        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF False] if_P[OF True]
   1.386 -          using `0 \<le> arctan x` by auto
   1.387 +        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 (- 1)\<close>] if_not_P[OF False] if_P[OF True]
   1.388 +          using \<open>0 \<le> arctan x\<close> by auto
   1.389        next
   1.390          case False
   1.391          hence "real ?invx \<le> 1" by auto
   1.392 -        have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \<le> real x`)
   1.393 -
   1.394 -        have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
   1.395 +        have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: \<open>0 \<le> real x\<close>)
   1.396 +
   1.397 +        have "1 / x \<noteq> 0" and "0 < 1 / x" using \<open>0 < real x\<close> by auto
   1.398  
   1.399          have "arctan (1 / x) \<le> arctan ?invx" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divr)
   1.400 -        also have "\<dots> \<le> ?ub_horner ?invx" using arctan_0_1_bounds_round[OF `0 \<le> real ?invx` `real ?invx \<le> 1`]
   1.401 +        also have "\<dots> \<le> ?ub_horner ?invx" using arctan_0_1_bounds_round[OF \<open>0 \<le> real ?invx\<close> \<open>real ?invx \<le> 1\<close>]
   1.402            by (auto intro!: float_round_up_le)
   1.403          also note float_round_up
   1.404          finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \<le> arctan x"
   1.405 -          using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
   1.406 -          unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
   1.407 +          using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
   1.408 +          unfolding real_sgn_pos[OF \<open>0 < 1 / real x\<close>] le_diff_eq by auto
   1.409          moreover
   1.410          have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
   1.411            unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
   1.412          ultimately
   1.413 -        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
   1.414 +        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 (- 1)\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 1\<close>] if_not_P[OF False]
   1.415            by (auto intro!: float_plus_down_le)
   1.416        qed
   1.417      qed
   1.418 @@ -764,7 +764,7 @@
   1.419  lemma ub_arctan_bound': assumes "0 \<le> real x"
   1.420    shows "arctan x \<le> ub_arctan prec x"
   1.421  proof -
   1.422 -  have "\<not> x < 0" and "0 \<le> x" using `0 \<le> real x` by auto
   1.423 +  have "\<not> x < 0" and "0 \<le> x" using \<open>0 \<le> real x\<close> by auto
   1.424  
   1.425    let "?ub_horner x" = "float_round_up prec (x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (float_round_down (Suc prec) (x * x)))"
   1.426      and "?lb_horner x" = "float_round_down prec (x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (float_round_up (Suc prec) (x * x)))"
   1.427 @@ -772,8 +772,8 @@
   1.428    show ?thesis
   1.429    proof (cases "x \<le> Float 1 (- 1)")
   1.430      case True hence "real x \<le> 1" by auto
   1.431 -    show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
   1.432 -      using arctan_0_1_bounds_round[OF `0 \<le> real x` `real x \<le> 1`]
   1.433 +    show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_P[OF True]
   1.434 +      using arctan_0_1_bounds_round[OF \<open>0 \<le> real x\<close> \<open>real x \<le> 1\<close>]
   1.435        by (auto intro!: float_round_up_le)
   1.436    next
   1.437      case False hence "0 < real x" by auto
   1.438 @@ -799,7 +799,7 @@
   1.439          truncate_down_nonneg add_nonneg_nonneg)
   1.440      have monotone: "x / ?R \<le> (float_divr prec x ?fR)"
   1.441      proof -
   1.442 -      from divide_left_mono[OF `?fR \<le> ?R` `0 \<le> real x` mult_pos_pos[OF divisor_gt0 `0 < real ?fR`]]
   1.443 +      from divide_left_mono[OF \<open>?fR \<le> ?R\<close> \<open>0 \<le> real x\<close> mult_pos_pos[OF divisor_gt0 \<open>0 < real ?fR\<close>]]
   1.444        have "x / ?R \<le> x / ?fR" .
   1.445        also have "\<dots> \<le> ?DIV" by (rule float_divr)
   1.446        finally show ?thesis .
   1.447 @@ -813,21 +813,21 @@
   1.448          case True
   1.449          have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
   1.450          from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
   1.451 -        show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
   1.452 +        show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 (- 1)\<close>] if_P[OF \<open>x \<le> Float 1 1\<close>] if_P[OF True] .
   1.453        next
   1.454          case False
   1.455          hence "real ?DIV \<le> 1" by auto
   1.456  
   1.457 -        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding zero_le_divide_iff by auto
   1.458 +        have "0 \<le> x / ?R" using \<open>0 \<le> real x\<close> \<open>0 < ?R\<close> unfolding zero_le_divide_iff by auto
   1.459          hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
   1.460  
   1.461          have "arctan x = 2 * arctan (x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
   1.462          also have "\<dots> \<le> 2 * arctan (?DIV)"
   1.463            using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
   1.464          also have "\<dots> \<le> (Float 1 1 * ?ub_horner ?DIV)" unfolding Float_num
   1.465 -          using arctan_0_1_bounds_round[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`]
   1.466 +          using arctan_0_1_bounds_round[OF \<open>0 \<le> real ?DIV\<close> \<open>real ?DIV \<le> 1\<close>]
   1.467            by (auto intro!: float_round_up_le)
   1.468 -        finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
   1.469 +        finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 (- 1)\<close>] if_P[OF \<open>x \<le> Float 1 1\<close>] if_not_P[OF False] .
   1.470        qed
   1.471      next
   1.472        case False
   1.473 @@ -837,23 +837,23 @@
   1.474        hence "0 < x" by auto
   1.475  
   1.476        let "?invx" = "float_divl prec 1 x"
   1.477 -      have "0 \<le> arctan x" using arctan_monotone'[OF `0 \<le> real x`] using arctan_tan[of 0, unfolded tan_zero] by auto
   1.478 -
   1.479 -      have "real ?invx \<le> 1" unfolding less_float_def by (rule order_trans[OF float_divl], auto simp add: `1 \<le> real x` divide_le_eq_1_pos[OF `0 < real x`])
   1.480 -      have "0 \<le> real ?invx" using `0 < x` by (intro float_divl_lower_bound) auto
   1.481 -
   1.482 -      have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
   1.483 -
   1.484 -      have "(?lb_horner ?invx) \<le> arctan (?invx)" using arctan_0_1_bounds_round[OF `0 \<le> real ?invx` `real ?invx \<le> 1`]
   1.485 +      have "0 \<le> arctan x" using arctan_monotone'[OF \<open>0 \<le> real x\<close>] using arctan_tan[of 0, unfolded tan_zero] by auto
   1.486 +
   1.487 +      have "real ?invx \<le> 1" unfolding less_float_def by (rule order_trans[OF float_divl], auto simp add: \<open>1 \<le> real x\<close> divide_le_eq_1_pos[OF \<open>0 < real x\<close>])
   1.488 +      have "0 \<le> real ?invx" using \<open>0 < x\<close> by (intro float_divl_lower_bound) auto
   1.489 +
   1.490 +      have "1 / x \<noteq> 0" and "0 < 1 / x" using \<open>0 < real x\<close> by auto
   1.491 +
   1.492 +      have "(?lb_horner ?invx) \<le> arctan (?invx)" using arctan_0_1_bounds_round[OF \<open>0 \<le> real ?invx\<close> \<open>real ?invx \<le> 1\<close>]
   1.493          by (auto intro!: float_round_down_le)
   1.494        also have "\<dots> \<le> arctan (1 / x)" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divl)
   1.495        finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
   1.496 -        using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
   1.497 -        unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
   1.498 +        using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
   1.499 +        unfolding real_sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
   1.500        moreover
   1.501        have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
   1.502        ultimately
   1.503 -      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`]if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF False]
   1.504 +      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>]if_not_P[OF \<open>\<not> x \<le> Float 1 (- 1)\<close>] if_not_P[OF False]
   1.505          by (auto intro!: float_round_up_le float_plus_up_le)
   1.506      qed
   1.507    qed
   1.508 @@ -863,13 +863,13 @@
   1.509    "arctan x \<in> {(lb_arctan prec x) .. (ub_arctan prec x)}"
   1.510  proof (cases "0 \<le> x")
   1.511    case True hence "0 \<le> real x" by auto
   1.512 -  show ?thesis using ub_arctan_bound'[OF `0 \<le> real x`] lb_arctan_bound'[OF `0 \<le> real x`] unfolding atLeastAtMost_iff by auto
   1.513 +  show ?thesis using ub_arctan_bound'[OF \<open>0 \<le> real x\<close>] lb_arctan_bound'[OF \<open>0 \<le> real x\<close>] unfolding atLeastAtMost_iff by auto
   1.514  next
   1.515    let ?mx = "-x"
   1.516    case False hence "x < 0" and "0 \<le> real ?mx" by auto
   1.517    hence bounds: "lb_arctan prec ?mx \<le> arctan ?mx \<and> arctan ?mx \<le> ub_arctan prec ?mx"
   1.518 -    using ub_arctan_bound'[OF `0 \<le> real ?mx`] lb_arctan_bound'[OF `0 \<le> real ?mx`] by auto
   1.519 -  show ?thesis unfolding minus_float.rep_eq arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
   1.520 +    using ub_arctan_bound'[OF \<open>0 \<le> real ?mx\<close>] lb_arctan_bound'[OF \<open>0 \<le> real ?mx\<close>] by auto
   1.521 +  show ?thesis unfolding minus_float.rep_eq arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF \<open>x < 0\<close>]
   1.522      unfolding atLeastAtMost_iff using bounds[unfolded minus_float.rep_eq arctan_minus]
   1.523      by (simp add: arctan_minus)
   1.524  qed
   1.525 @@ -919,7 +919,7 @@
   1.526        unfolding F by auto } note f_eq = this
   1.527  
   1.528    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
   1.529 -    OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
   1.530 +    OF \<open>0 \<le> real (x * x)\<close> f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
   1.531    show "?lb" and "?ub" by (auto simp add: power_mult power2_eq_square[of "real x"])
   1.532  qed
   1.533  
   1.534 @@ -934,8 +934,8 @@
   1.535    shows "cos x \<in> {(lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) .. (ub_sin_cos_aux prec (get_odd n) 1 1 (x * x))}"
   1.536  proof (cases "real x = 0")
   1.537    case False hence "real x \<noteq> 0" by auto
   1.538 -  hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   1.539 -  have "0 < x * x" using `0 < x` by simp
   1.540 +  hence "0 < x" and "0 < real x" using \<open>0 \<le> real x\<close> by auto
   1.541 +  have "0 < x * x" using \<open>0 < x\<close> by simp
   1.542  
   1.543    { fix x n have "(\<Sum> i=0..<n. (-1::real) ^ i * (1/(fact (2 * i))) * x ^ (2 * i))
   1.544      = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/((fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
   1.545 @@ -957,7 +957,7 @@
   1.546        cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/((fact i)) else 0) * (real x) ^ i)
   1.547        + (cos (t + 1/2 * (2 * n) * pi) / (fact (2*n))) * (real x)^(2*n)"
   1.548        (is "_ = ?SUM + ?rest / ?fact * ?pow")
   1.549 -      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
   1.550 +      using Maclaurin_cos_expansion2[OF \<open>0 < real x\<close> \<open>0 < 2 * n\<close>]
   1.551        unfolding cos_coeff_def atLeast0LessThan by auto
   1.552  
   1.553      have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
   1.554 @@ -965,12 +965,12 @@
   1.555      also have "\<dots> = ?rest" by auto
   1.556      finally have "cos t * (- 1) ^ n = ?rest" .
   1.557      moreover
   1.558 -    have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
   1.559 -    hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
   1.560 +    have "t \<le> pi / 2" using \<open>t < real x\<close> and \<open>x \<le> pi / 2\<close> by auto
   1.561 +    hence "0 \<le> cos t" using \<open>0 < t\<close> and cos_ge_zero by auto
   1.562      ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
   1.563  
   1.564      have "0 < ?fact" by auto
   1.565 -    have "0 < ?pow" using `0 < real x` by auto
   1.566 +    have "0 < ?pow" using \<open>0 < real x\<close> by auto
   1.567  
   1.568      {
   1.569        assume "even n"
   1.570 @@ -978,7 +978,7 @@
   1.571          unfolding morph_to_if_power[symmetric] using cos_aux by auto
   1.572        also have "\<dots> \<le> cos x"
   1.573        proof -
   1.574 -        from even[OF `even n`] `0 < ?fact` `0 < ?pow`
   1.575 +        from even[OF \<open>even n\<close>] \<open>0 < ?fact\<close> \<open>0 < ?pow\<close>
   1.576          have "0 \<le> (?rest / ?fact) * ?pow" by simp
   1.577          thus ?thesis unfolding cos_eq by auto
   1.578        qed
   1.579 @@ -989,7 +989,7 @@
   1.580        assume "odd n"
   1.581        have "cos x \<le> ?SUM"
   1.582        proof -
   1.583 -        from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`]
   1.584 +        from \<open>0 < ?fact\<close> and \<open>0 < ?pow\<close> and odd[OF \<open>odd n\<close>]
   1.585          have "0 \<le> (- ?rest) / ?fact * ?pow"
   1.586            by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
   1.587          thus ?thesis unfolding cos_eq by auto
   1.588 @@ -1007,9 +1007,9 @@
   1.589    next
   1.590      case False
   1.591      hence "get_even n = 0" by auto
   1.592 -    have "- (pi / 2) \<le> x" by (rule order_trans[OF _ `0 < real x`[THEN less_imp_le]], auto)
   1.593 -    with `x \<le> pi / 2`
   1.594 -    show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps minus_float.rep_eq zero_float.rep_eq using cos_ge_zero by auto
   1.595 +    have "- (pi / 2) \<le> x" by (rule order_trans[OF _ \<open>0 < real x\<close>[THEN less_imp_le]], auto)
   1.596 +    with \<open>x \<le> pi / 2\<close>
   1.597 +    show ?thesis unfolding \<open>get_even n = 0\<close> lb_sin_cos_aux.simps minus_float.rep_eq zero_float.rep_eq using cos_ge_zero by auto
   1.598    qed
   1.599    ultimately show ?thesis by auto
   1.600  next
   1.601 @@ -1034,8 +1034,8 @@
   1.602        unfolding F by auto }
   1.603    note f_eq = this
   1.604    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
   1.605 -    OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
   1.606 -  show "?lb" and "?ub" using `0 \<le> real x`
   1.607 +    OF \<open>0 \<le> real (x * x)\<close> f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
   1.608 +  show "?lb" and "?ub" using \<open>0 \<le> real x\<close>
   1.609      unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
   1.610      unfolding mult.commute[where 'a=real] real_fact_nat
   1.611      by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"])
   1.612 @@ -1045,8 +1045,8 @@
   1.613    shows "sin x \<in> {(x * lb_sin_cos_aux prec (get_even n) 2 1 (x * x)) .. (x * ub_sin_cos_aux prec (get_odd n) 2 1 (x * x))}"
   1.614  proof (cases "real x = 0")
   1.615    case False hence "real x \<noteq> 0" by auto
   1.616 -  hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   1.617 -  have "0 < x * x" using `0 < x` by simp
   1.618 +  hence "0 < x" and "0 < real x" using \<open>0 \<le> real x\<close> by auto
   1.619 +  have "0 < x * x" using \<open>0 < x\<close> by simp
   1.620  
   1.621    { fix x::real and n
   1.622      have "(\<Sum>j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / ((fact (2 * j + 1))) * x ^(2 * j + 1))
   1.623 @@ -1067,27 +1067,27 @@
   1.624        sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)
   1.625        + (sin (t + 1/2 * (2 * n + 1) * pi) / (fact (2*n + 1))) * (real x)^(2*n + 1)"
   1.626        (is "_ = ?SUM + ?rest / ?fact * ?pow")
   1.627 -      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
   1.628 +      using Maclaurin_sin_expansion3[OF \<open>0 < 2 * n + 1\<close> \<open>0 < real x\<close>]
   1.629        unfolding sin_coeff_def atLeast0LessThan by auto
   1.630  
   1.631      have "?rest = cos t * (- 1) ^ n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
   1.632      moreover
   1.633 -    have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
   1.634 -    hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
   1.635 +    have "t \<le> pi / 2" using \<open>t < real x\<close> and \<open>x \<le> pi / 2\<close> by auto
   1.636 +    hence "0 \<le> cos t" using \<open>0 < t\<close> and cos_ge_zero by auto
   1.637      ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
   1.638  
   1.639      have "0 < ?fact" by (simp del: fact_Suc)
   1.640 -    have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
   1.641 +    have "0 < ?pow" using \<open>0 < real x\<close> by (rule zero_less_power)
   1.642  
   1.643      {
   1.644        assume "even n"
   1.645        have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
   1.646              (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)"
   1.647 -        using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
   1.648 +        using sin_aux[OF \<open>0 \<le> real x\<close>] unfolding setsum_morph[symmetric] by auto
   1.649        also have "\<dots> \<le> ?SUM" by auto
   1.650        also have "\<dots> \<le> sin x"
   1.651        proof -
   1.652 -        from even[OF `even n`] `0 < ?fact` `0 < ?pow`
   1.653 +        from even[OF \<open>even n\<close>] \<open>0 < ?fact\<close> \<open>0 < ?pow\<close>
   1.654          have "0 \<le> (?rest / ?fact) * ?pow" by simp
   1.655          thus ?thesis unfolding sin_eq by auto
   1.656        qed
   1.657 @@ -1098,7 +1098,7 @@
   1.658        assume "odd n"
   1.659        have "sin x \<le> ?SUM"
   1.660        proof -
   1.661 -        from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`]
   1.662 +        from \<open>0 < ?fact\<close> and \<open>0 < ?pow\<close> and odd[OF \<open>odd n\<close>]
   1.663          have "0 \<le> (- ?rest) / ?fact * ?pow"
   1.664            by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
   1.665          thus ?thesis unfolding sin_eq by auto
   1.666 @@ -1106,7 +1106,7 @@
   1.667        also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)"
   1.668           by auto
   1.669        also have "\<dots> \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))"
   1.670 -        using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
   1.671 +        using sin_aux[OF \<open>0 \<le> real x\<close>] unfolding setsum_morph[symmetric] by auto
   1.672        finally have "sin x \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" .
   1.673      } note ub = this and lb
   1.674    } note ub = this(1) and lb = this(2)
   1.675 @@ -1118,8 +1118,8 @@
   1.676    next
   1.677      case False
   1.678      hence "get_even n = 0" by auto
   1.679 -    with `x \<le> pi / 2` `0 \<le> real x`
   1.680 -    show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps minus_float.rep_eq using sin_ge_zero by auto
   1.681 +    with \<open>x \<le> pi / 2\<close> \<open>0 \<le> real x\<close>
   1.682 +    show ?thesis unfolding \<open>get_even n = 0\<close> ub_sin_cos_aux.simps minus_float.rep_eq using sin_ge_zero by auto
   1.683    qed
   1.684    ultimately show ?thesis by auto
   1.685  next
   1.686 @@ -1127,10 +1127,10 @@
   1.687    show ?thesis
   1.688    proof (cases "n = 0")
   1.689      case True
   1.690 -    thus ?thesis unfolding `n = 0` get_even_def get_odd_def using `real x = 0` lapprox_rat[where x="-1" and y=1] by auto
   1.691 +    thus ?thesis unfolding \<open>n = 0\<close> get_even_def get_odd_def using \<open>real x = 0\<close> lapprox_rat[where x="-1" and y=1] by auto
   1.692    next
   1.693      case False with not0_implies_Suc obtain m where "n = Suc m" by blast
   1.694 -    thus ?thesis unfolding `n = Suc m` get_even_def get_odd_def using `real x = 0` rapprox_rat[where x=1 and y=1] lapprox_rat[where x=1 and y=1] by (cases "even (Suc m)", auto)
   1.695 +    thus ?thesis unfolding \<open>n = Suc m\<close> get_even_def get_odd_def using \<open>real x = 0\<close> rapprox_rat[where x=1 and y=1] lapprox_rat[where x=1 and y=1] by (cases "even (Suc m)", auto)
   1.696    qed
   1.697  qed
   1.698  
   1.699 @@ -1163,7 +1163,7 @@
   1.700      finally have "cos x = 2 * cos (x / 2) * cos (x / 2) - 1" .
   1.701    } note x_half = this[symmetric]
   1.702  
   1.703 -  have "\<not> x < 0" using `0 \<le> real x` by auto
   1.704 +  have "\<not> x < 0" using \<open>0 \<le> real x\<close> by auto
   1.705    let "?ub_horner x" = "ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 1 1 (x * x)"
   1.706    let "?lb_horner x" = "lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 1 1 (x * x)"
   1.707    let "?ub_half x" = "float_plus_up prec (Float 1 1 * x * x) (- 1)"
   1.708 @@ -1172,8 +1172,8 @@
   1.709    show ?thesis
   1.710    proof (cases "x < Float 1 (- 1)")
   1.711      case True hence "x \<le> pi / 2" using pi_ge_two by auto
   1.712 -    show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 (- 1)`] Let_def
   1.713 -      using cos_boundaries[OF `0 \<le> real x` `x \<le> pi / 2`] .
   1.714 +    show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF \<open>\<not> x < 0\<close>] if_P[OF \<open>x < Float 1 (- 1)\<close>] Let_def
   1.715 +      using cos_boundaries[OF \<open>0 \<le> real x\<close> \<open>x \<le> pi / 2\<close>] .
   1.716    next
   1.717      case False
   1.718      { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
   1.719 @@ -1187,7 +1187,7 @@
   1.720        next
   1.721          case False
   1.722          hence "0 \<le> real y" by auto
   1.723 -        from mult_mono[OF `y \<le> cos ?x2` `y \<le> cos ?x2` `0 \<le> cos ?x2` this]
   1.724 +        from mult_mono[OF \<open>y \<le> cos ?x2\<close> \<open>y \<le> cos ?x2\<close> \<open>0 \<le> cos ?x2\<close> this]
   1.725          have "real y * real y \<le> cos ?x2 * cos ?x2" .
   1.726          hence "2 * real y * real y \<le> 2 * cos ?x2 * cos ?x2" by auto
   1.727          hence "2 * real y * real y - 1 \<le> 2 * cos (x / 2) * cos (x / 2) - 1" unfolding Float_num by auto
   1.728 @@ -1203,8 +1203,8 @@
   1.729  
   1.730        have "cos x \<le> (?ub_half y)"
   1.731        proof -
   1.732 -        have "0 \<le> real y" using `0 \<le> cos ?x2` ub by (rule order_trans)
   1.733 -        from mult_mono[OF ub ub this `0 \<le> cos ?x2`]
   1.734 +        have "0 \<le> real y" using \<open>0 \<le> cos ?x2\<close> ub by (rule order_trans)
   1.735 +        from mult_mono[OF ub ub this \<open>0 \<le> cos ?x2\<close>]
   1.736          have "cos ?x2 * cos ?x2 \<le> real y * real y" .
   1.737          hence "2 * cos ?x2 * cos ?x2 \<le> 2 * real y * real y" by auto
   1.738          hence "2 * cos (x / 2) * cos (x / 2) - 1 \<le> 2 * real y * real y - 1" unfolding Float_num by auto
   1.739 @@ -1216,29 +1216,29 @@
   1.740      let ?x2 = "x * Float 1 (- 1)"
   1.741      let ?x4 = "x * Float 1 (- 1) * Float 1 (- 1)"
   1.742  
   1.743 -    have "-pi \<le> x" using pi_ge_zero[THEN le_imp_neg_le, unfolded minus_zero] `0 \<le> real x` by (rule order_trans)
   1.744 +    have "-pi \<le> x" using pi_ge_zero[THEN le_imp_neg_le, unfolded minus_zero] \<open>0 \<le> real x\<close> by (rule order_trans)
   1.745  
   1.746      show ?thesis
   1.747      proof (cases "x < 1")
   1.748        case True hence "real x \<le> 1" by auto
   1.749 -      have "0 \<le> real ?x2" and "?x2 \<le> pi / 2" using pi_ge_two `0 \<le> real x` using assms by auto
   1.750 +      have "0 \<le> real ?x2" and "?x2 \<le> pi / 2" using pi_ge_two \<open>0 \<le> real x\<close> using assms by auto
   1.751        from cos_boundaries[OF this]
   1.752        have lb: "(?lb_horner ?x2) \<le> ?cos ?x2" and ub: "?cos ?x2 \<le> (?ub_horner ?x2)" by auto
   1.753  
   1.754        have "(?lb x) \<le> ?cos x"
   1.755        proof -
   1.756 -        from lb_half[OF lb `-pi \<le> x` `x \<le> pi`]
   1.757 -        show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
   1.758 +        from lb_half[OF lb \<open>-pi \<le> x\<close> \<open>x \<le> pi\<close>]
   1.759 +        show ?thesis unfolding lb_cos_def[where x=x] Let_def using \<open>\<not> x < 0\<close> \<open>\<not> x < Float 1 (- 1)\<close> \<open>x < 1\<close> by auto
   1.760        qed
   1.761        moreover have "?cos x \<le> (?ub x)"
   1.762        proof -
   1.763 -        from ub_half[OF ub `-pi \<le> x` `x \<le> pi`]
   1.764 -        show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
   1.765 +        from ub_half[OF ub \<open>-pi \<le> x\<close> \<open>x \<le> pi\<close>]
   1.766 +        show ?thesis unfolding ub_cos_def[where x=x] Let_def using \<open>\<not> x < 0\<close> \<open>\<not> x < Float 1 (- 1)\<close> \<open>x < 1\<close> by auto
   1.767        qed
   1.768        ultimately show ?thesis by auto
   1.769      next
   1.770        case False
   1.771 -      have "0 \<le> real ?x4" and "?x4 \<le> pi / 2" using pi_ge_two `0 \<le> real x` `x \<le> pi` unfolding Float_num by auto
   1.772 +      have "0 \<le> real ?x4" and "?x4 \<le> pi / 2" using pi_ge_two \<open>0 \<le> real x\<close> \<open>x \<le> pi\<close> unfolding Float_num by auto
   1.773        from cos_boundaries[OF this]
   1.774        have lb: "(?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> (?ub_horner ?x4)" by auto
   1.775  
   1.776 @@ -1246,15 +1246,15 @@
   1.777  
   1.778        have "(?lb x) \<le> ?cos x"
   1.779        proof -
   1.780 -        have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` `x \<le> pi` by auto
   1.781 -        from lb_half[OF lb_half[OF lb this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
   1.782 -        show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 (- 1)`] if_not_P[OF `\<not> x < 1`] Let_def .
   1.783 +        have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two \<open>0 \<le> real x\<close> \<open>x \<le> pi\<close> by auto
   1.784 +        from lb_half[OF lb_half[OF lb this] \<open>-pi \<le> x\<close> \<open>x \<le> pi\<close>, unfolded eq_4]
   1.785 +        show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x < Float 1 (- 1)\<close>] if_not_P[OF \<open>\<not> x < 1\<close>] Let_def .
   1.786        qed
   1.787        moreover have "?cos x \<le> (?ub x)"
   1.788        proof -
   1.789 -        have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` ` x \<le> pi` by auto
   1.790 -        from ub_half[OF ub_half[OF ub this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
   1.791 -        show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 (- 1)`] if_not_P[OF `\<not> x < 1`] Let_def .
   1.792 +        have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two \<open>0 \<le> real x\<close> \<open> x \<le> pi\<close> by auto
   1.793 +        from ub_half[OF ub_half[OF ub this] \<open>-pi \<le> x\<close> \<open>x \<le> pi\<close>, unfolded eq_4]
   1.794 +        show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF \<open>\<not> x < 0\<close>] if_not_P[OF \<open>\<not> x < Float 1 (- 1)\<close>] if_not_P[OF \<open>\<not> x < 1\<close>] Let_def .
   1.795        qed
   1.796        ultimately show ?thesis by auto
   1.797      qed
   1.798 @@ -1264,7 +1264,7 @@
   1.799  lemma lb_cos_minus: assumes "-pi \<le> x" and "real x \<le> 0"
   1.800    shows "cos (real(-x)) \<in> {(lb_cos prec (-x)) .. (ub_cos prec (-x))}"
   1.801  proof -
   1.802 -  have "0 \<le> real (-x)" and "(-x) \<le> pi" using `-pi \<le> x` `real x \<le> 0` by auto
   1.803 +  have "0 \<le> real (-x)" and "(-x) \<le> pi" using \<open>-pi \<le> x\<close> \<open>real x \<le> 0\<close> by auto
   1.804    from lb_cos[OF this] show ?thesis .
   1.805  qed
   1.806  
   1.807 @@ -1562,8 +1562,8 @@
   1.808        have "(get_odd n) \<noteq> 0" using get_odd[THEN odd_pos] by auto
   1.809        thus ?thesis unfolding True power_0_left by auto
   1.810      next
   1.811 -      case False hence "real x < 0" using `real x \<le> 0` by auto
   1.812 -      show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq `real x < 0`)
   1.813 +      case False hence "real x < 0" using \<open>real x \<le> 0\<close> by auto
   1.814 +      show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq \<open>real x < 0\<close>)
   1.815      qed
   1.816  
   1.817      obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / (fact m)) + exp t / (fact (get_odd n)) * (real x) ^ (get_odd n)"
   1.818 @@ -1624,12 +1624,12 @@
   1.819    let "?horner x" = "let  y = ?lb_horner x  in if y \<le> 0 then Float 1 (- 2) else y"
   1.820    have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto)
   1.821    moreover { fix x :: float fix num :: nat
   1.822 -    have "0 < real (?horner x) ^ num" using `0 < ?horner x` by simp
   1.823 +    have "0 < real (?horner x) ^ num" using \<open>0 < ?horner x\<close> by simp
   1.824      also have "\<dots> = (?horner x) ^ num" by auto
   1.825      finally have "0 < real ((?horner x) ^ num)" .
   1.826    }
   1.827    ultimately show ?thesis
   1.828 -    unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def
   1.829 +    unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] Let_def
   1.830      by (cases "floor_fl x", cases "x < - 1", auto simp: real_power_up_fl real_power_down_fl
   1.831        intro!: power_up_less power_down_pos)
   1.832  qed
   1.833 @@ -1640,27 +1640,27 @@
   1.834    let "?lb_exp_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
   1.835    let "?ub_exp_horner x" = "ub_exp_horner prec (get_odd (prec + 2)) 1 1 x"
   1.836  
   1.837 -  have "real x \<le> 0" and "\<not> x > 0" using `x \<le> 0` by auto
   1.838 +  have "real x \<le> 0" and "\<not> x > 0" using \<open>x \<le> 0\<close> by auto
   1.839    show ?thesis
   1.840    proof (cases "x < - 1")
   1.841      case False hence "- 1 \<le> real x" by auto
   1.842      show ?thesis
   1.843      proof (cases "?lb_exp_horner x \<le> 0")
   1.844 -      from `\<not> x < - 1` have "- 1 \<le> real x" by auto
   1.845 +      from \<open>\<not> x < - 1\<close> have "- 1 \<le> real x" by auto
   1.846        hence "exp (- 1) \<le> exp x" unfolding exp_le_cancel_iff .
   1.847        from order_trans[OF exp_m1_ge_quarter this]
   1.848        have "Float 1 (- 2) \<le> exp x" unfolding Float_num .
   1.849        moreover case True
   1.850 -      ultimately show ?thesis using bnds_exp_horner `real x \<le> 0` `\<not> x > 0` `\<not> x < - 1` by auto
   1.851 +      ultimately show ?thesis using bnds_exp_horner \<open>real x \<le> 0\<close> \<open>\<not> x > 0\<close> \<open>\<not> x < - 1\<close> by auto
   1.852      next
   1.853 -      case False thus ?thesis using bnds_exp_horner `real x \<le> 0` `\<not> x > 0` `\<not> x < - 1` by (auto simp add: Let_def)
   1.854 +      case False thus ?thesis using bnds_exp_horner \<open>real x \<le> 0\<close> \<open>\<not> x > 0\<close> \<open>\<not> x < - 1\<close> by (auto simp add: Let_def)
   1.855      qed
   1.856    next
   1.857      case True
   1.858  
   1.859      let ?num = "nat (- int_floor_fl x)"
   1.860  
   1.861 -    have "real (int_floor_fl x) < - 1" using int_floor_fl[of x] `x < - 1`
   1.862 +    have "real (int_floor_fl x) < - 1" using int_floor_fl[of x] \<open>x < - 1\<close>
   1.863        by simp
   1.864      hence "real (int_floor_fl x) < 0" by simp
   1.865      hence "int_floor_fl x < 0" by auto
   1.866 @@ -1668,22 +1668,22 @@
   1.867      hence "0 < nat (- int_floor_fl x)" by auto
   1.868      hence "0 < ?num"  by auto
   1.869      hence "real ?num \<noteq> 0" by auto
   1.870 -    have num_eq: "real ?num = - int_floor_fl x" using `0 < nat (- int_floor_fl x)` by auto
   1.871 -    have "0 < - int_floor_fl x" using `0 < ?num`[unfolded real_of_nat_less_iff[symmetric]] by simp
   1.872 +    have num_eq: "real ?num = - int_floor_fl x" using \<open>0 < nat (- int_floor_fl x)\<close> by auto
   1.873 +    have "0 < - int_floor_fl x" using \<open>0 < ?num\<close>[unfolded real_of_nat_less_iff[symmetric]] by simp
   1.874      hence "real (int_floor_fl x) < 0" unfolding less_float_def by auto
   1.875      have fl_eq: "real (- int_floor_fl x) = real (- floor_fl x)"
   1.876        by (simp add: floor_fl_def int_floor_fl_def)
   1.877 -    from `0 < - int_floor_fl x` have "0 \<le> real (- floor_fl x)"
   1.878 +    from \<open>0 < - int_floor_fl x\<close> have "0 \<le> real (- floor_fl x)"
   1.879        by (simp add: floor_fl_def int_floor_fl_def)
   1.880 -    from `real (int_floor_fl x) < 0` have "real (floor_fl x) < 0"
   1.881 +    from \<open>real (int_floor_fl x) < 0\<close> have "real (floor_fl x) < 0"
   1.882        by (simp add: floor_fl_def int_floor_fl_def)
   1.883      have "exp x \<le> ub_exp prec x"
   1.884      proof -
   1.885        have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
   1.886 -        using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 \<le> real (- floor_fl x)`]
   1.887 +        using float_divr_nonpos_pos_upper_bound[OF \<open>real x \<le> 0\<close> \<open>0 \<le> real (- floor_fl x)\<close>]
   1.888          unfolding less_eq_float_def zero_float.rep_eq .
   1.889  
   1.890 -      have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
   1.891 +      have "exp x = exp (?num * (x / ?num))" using \<open>real ?num \<noteq> 0\<close> by auto
   1.892        also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
   1.893        also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num" unfolding num_eq fl_eq
   1.894          by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
   1.895 @@ -1692,7 +1692,7 @@
   1.896          by (rule power_mono, rule bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct2], auto)
   1.897        also have "\<dots> \<le> real (power_up_fl prec (?ub_exp_horner (float_divr prec x (- floor_fl x))) ?num)"
   1.898          by (auto simp add: real_power_up_fl intro!: power_up ub_exp_horner_nonneg div_less_zero)
   1.899 -      finally show ?thesis unfolding ub_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] floor_fl_def Let_def
   1.900 +      finally show ?thesis unfolding ub_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>] floor_fl_def Let_def
   1.901          .
   1.902      qed
   1.903      moreover
   1.904 @@ -1706,17 +1706,17 @@
   1.905          case False hence "0 \<le> real ?horner" by auto
   1.906  
   1.907          have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
   1.908 -          using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
   1.909 +          using \<open>real (floor_fl x) < 0\<close> \<open>real x \<le> 0\<close> by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
   1.910  
   1.911          have "(?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num \<le>
   1.912            exp (float_divl prec x (- floor_fl x)) ^ ?num"
   1.913 -          using `0 \<le> real ?horner`[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
   1.914 +          using \<open>0 \<le> real ?horner\<close>[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
   1.915          also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
   1.916            using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
   1.917          also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
   1.918 -        also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
   1.919 +        also have "\<dots> = exp x" using \<open>real ?num \<noteq> 0\<close> by auto
   1.920          finally show ?thesis using False
   1.921 -          unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_not_P[OF False]
   1.922 +          unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>] int_floor_fl_def Let_def if_not_P[OF False]
   1.923            by (auto simp: real_power_down_fl intro!: power_down_le)
   1.924        next
   1.925          case True
   1.926 @@ -1725,16 +1725,16 @@
   1.927          then have "power_down_fl prec (Float 1 (- 2))  ?num \<le> real (Float 1 (- 2)) ^ ?num"
   1.928            by simp
   1.929          also
   1.930 -        have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
   1.931 -        from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
   1.932 +        have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using \<open>real (floor_fl x) < 0\<close> by auto
   1.933 +        from divide_right_mono_neg[OF floor_fl[of x] \<open>real (floor_fl x) \<le> 0\<close>, unfolded divide_self[OF \<open>real (floor_fl x) \<noteq> 0\<close>]]
   1.934          have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
   1.935          from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
   1.936          have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
   1.937          hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
   1.938            by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
   1.939 -        also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
   1.940 +        also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using \<open>real (floor_fl x) \<noteq> 0\<close> by auto
   1.941          finally show ?thesis
   1.942 -          unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power
   1.943 +          unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>] int_floor_fl_def Let_def if_P[OF True] real_of_float_power
   1.944            .
   1.945        qed
   1.946      qed
   1.947 @@ -1753,7 +1753,7 @@
   1.948  
   1.949      have "lb_exp prec x \<le> exp x"
   1.950      proof -
   1.951 -      from exp_boundaries'[OF `-x \<le> 0`]
   1.952 +      from exp_boundaries'[OF \<open>-x \<le> 0\<close>]
   1.953        have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
   1.954  
   1.955        have "float_divl prec 1 (ub_exp prec (-x)) \<le> 1 / ub_exp prec (-x)" using float_divl[where x=1] by auto
   1.956 @@ -1765,13 +1765,13 @@
   1.957      moreover
   1.958      have "exp x \<le> ub_exp prec x"
   1.959      proof -
   1.960 -      have "\<not> 0 < -x" using `0 < x` by auto
   1.961 -
   1.962 -      from exp_boundaries'[OF `-x \<le> 0`]
   1.963 +      have "\<not> 0 < -x" using \<open>0 < x\<close> by auto
   1.964 +
   1.965 +      from exp_boundaries'[OF \<open>-x \<le> 0\<close>]
   1.966        have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
   1.967  
   1.968        have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
   1.969 -        using lb_exp lb_exp_pos[OF `\<not> 0 < -x`, of prec]
   1.970 +        using lb_exp lb_exp_pos[OF \<open>\<not> 0 < -x\<close>, of prec]
   1.971          by (simp del: lb_exp.simps add: exp_minus inverse_eq_divide field_simps)
   1.972        also have "\<dots> \<le> float_divr prec 1 (lb_exp prec (-x))" using float_divr .
   1.973        finally show ?thesis unfolding ub_exp.simps if_P[OF True] .
   1.974 @@ -1818,20 +1818,20 @@
   1.975    let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
   1.976  
   1.977    have ln_eq: "(\<Sum> i. (- 1) ^ i * ?a i) = ln (x + 1)"
   1.978 -    using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
   1.979 +    using ln_series[of "x + 1"] \<open>0 \<le> x\<close> \<open>x < 1\<close> by auto
   1.980  
   1.981    have "norm x < 1" using assms by auto
   1.982    have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
   1.983 -    using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
   1.984 -  { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto simp: `0 \<le> x`) }
   1.985 +    using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF \<open>norm x < 1\<close>]]] by auto
   1.986 +  { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto simp: \<open>0 \<le> x\<close>) }
   1.987    { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
   1.988      proof (rule mult_mono)
   1.989 -      show "0 \<le> x ^ Suc (Suc n)" by (auto simp add: `0 \<le> x`)
   1.990 +      show "0 \<le> x ^ Suc (Suc n)" by (auto simp add: \<open>0 \<le> x\<close>)
   1.991        have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult.assoc[symmetric]
   1.992 -        by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto simp: `0 \<le> x`)
   1.993 +        by (rule mult_left_mono, fact less_imp_le[OF \<open>x < 1\<close>], auto simp: \<open>0 \<le> x\<close>)
   1.994        thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
   1.995      qed auto }
   1.996 -  from summable_Leibniz'(2,4)[OF `?a ----> 0` `\<And>n. 0 \<le> ?a n`, OF `\<And>n. ?a (Suc n) \<le> ?a n`, unfolded ln_eq]
   1.997 +  from summable_Leibniz'(2,4)[OF \<open>?a ----> 0\<close> \<open>\<And>n. 0 \<le> ?a n\<close>, OF \<open>\<And>n. ?a (Suc n) \<le> ?a n\<close>, unfolded ln_eq]
   1.998    show "?lb" and "?ub" unfolding atLeast0LessThan by auto
   1.999  qed
  1.1000  
  1.1001 @@ -1847,15 +1847,15 @@
  1.1002  
  1.1003    have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult.commute[of "real x"] ev
  1.1004      using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
  1.1005 -      OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
  1.1006 +      OF \<open>0 \<le> real x\<close> refl lb_ln_horner.simps ub_ln_horner.simps] \<open>0 \<le> real x\<close>
  1.1007      by (rule mult_right_mono)
  1.1008 -  also have "\<dots> \<le> ?ln" using ln_bounds(1)[OF `0 \<le> real x` `real x < 1`] by auto
  1.1009 +  also have "\<dots> \<le> ?ln" using ln_bounds(1)[OF \<open>0 \<le> real x\<close> \<open>real x < 1\<close>] by auto
  1.1010    finally show "?lb \<le> ?ln" .
  1.1011  
  1.1012 -  have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
  1.1013 +  have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF \<open>0 \<le> real x\<close> \<open>real x < 1\<close>] by auto
  1.1014    also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult.commute[of "real x"] od
  1.1015      using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
  1.1016 -      OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
  1.1017 +      OF \<open>0 \<le> real x\<close> refl lb_ln_horner.simps ub_ln_horner.simps] \<open>0 \<le> real x\<close>
  1.1018      by (rule mult_right_mono)
  1.1019    finally show "?ln \<le> ?ub" .
  1.1020  qed
  1.1021 @@ -1864,7 +1864,7 @@
  1.1022    fixes x::real assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
  1.1023  proof -
  1.1024    have "x \<noteq> 0" using assms by auto
  1.1025 -  have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
  1.1026 +  have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF \<open>x \<noteq> 0\<close>] by auto
  1.1027    moreover
  1.1028    have "0 < y / x" using assms by auto
  1.1029    hence "0 < 1 + y / x" by auto
  1.1030 @@ -1947,13 +1947,13 @@
  1.1031  termination proof (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 1 then 1 else 0))", auto)
  1.1032    fix prec and x :: float assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divl (max prec (Suc 0)) 1 x) < 1"
  1.1033    hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1" by auto
  1.1034 -  from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`[THEN less_imp_le] `1 \<le> max prec (Suc 0)`]
  1.1035 -  show False using `real (float_divl (max prec (Suc 0)) 1 x) < 1` by auto
  1.1036 +  from float_divl_pos_less1_bound[OF \<open>0 < real x\<close> \<open>real x < 1\<close>[THEN less_imp_le] \<open>1 \<le> max prec (Suc 0)\<close>]
  1.1037 +  show False using \<open>real (float_divl (max prec (Suc 0)) 1 x) < 1\<close> by auto
  1.1038  next
  1.1039    fix prec x assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divr prec 1 x) < 1"
  1.1040    hence "0 < x" by auto
  1.1041 -  from float_divr_pos_less1_lower_bound[OF `0 < x`, of prec] `real x < 1`
  1.1042 -  show False using `real (float_divr prec 1 x) < 1` by auto
  1.1043 +  from float_divr_pos_less1_lower_bound[OF \<open>0 < x\<close>, of prec] \<open>real x < 1\<close>
  1.1044 +  show False using \<open>real (float_divr prec 1 x) < 1\<close> by auto
  1.1045  qed
  1.1046  
  1.1047  lemma float_pos_eq_mantissa_pos:  "x > 0 \<longleftrightarrow> mantissa x > 0"
  1.1048 @@ -1976,7 +1976,7 @@
  1.1049      using Float_pos_eq_mantissa_pos[of m e] float_pos_eq_mantissa_pos[of x] by simp_all
  1.1050    thus ?th1 using bitlen_Float[of m e] assms by (auto simp add: zero_less_mult_iff intro!: arg_cong2[where f=Float])
  1.1051    have "x \<noteq> float_of 0"
  1.1052 -    unfolding zero_float_def[symmetric] using `0 < x` by auto
  1.1053 +    unfolding zero_float_def[symmetric] using \<open>0 < x\<close> by auto
  1.1054    from denormalize_shift[OF assms(1) this] guess i . note i = this
  1.1055  
  1.1056    have "2 powr (1 - (real (bitlen (mantissa x)) + real i)) =
  1.1057 @@ -1984,7 +1984,7 @@
  1.1058      by (simp add: powr_minus[symmetric] powr_add[symmetric] field_simps)
  1.1059    hence "real (mantissa x) * 2 powr (1 - real (bitlen (mantissa x))) =
  1.1060      (real (mantissa x) * 2 ^ i) * 2 powr (1 - real (bitlen (mantissa x * 2 ^ i)))"
  1.1061 -    using `mantissa x > 0` by (simp add: powr_realpow)
  1.1062 +    using \<open>mantissa x > 0\<close> by (simp add: powr_realpow)
  1.1063    then show ?th2
  1.1064      unfolding i by transfer auto
  1.1065  qed
  1.1066 @@ -2025,7 +2025,7 @@
  1.1067    proof (cases "0 \<le> e")
  1.1068      case True
  1.1069      thus ?thesis
  1.1070 -      unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
  1.1071 +      unfolding bl_def[symmetric] using \<open>0 < real m\<close> \<open>0 \<le> bl\<close>
  1.1072        apply (simp add: ln_mult)
  1.1073        apply (cases "e=0")
  1.1074          apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr)
  1.1075 @@ -2036,7 +2036,7 @@
  1.1076      have lne: "ln (2 powr real e) = ln (inverse (2 powr - e))" by (simp add: powr_minus)
  1.1077      hence pow_gt0: "(0::real) < 2^nat (-e)" by auto
  1.1078      hence inv_gt0: "(0::real) < inverse (2^nat (-e))" by auto
  1.1079 -    show ?thesis using False unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
  1.1080 +    show ?thesis using False unfolding bl_def[symmetric] using \<open>0 < real m\<close> \<open>0 \<le> bl\<close>
  1.1081        by (auto simp add: lne ln_mult ln_powr ln_div field_simps)
  1.1082    qed
  1.1083  qed
  1.1084 @@ -2047,8 +2047,8 @@
  1.1085  proof (cases "x < Float 1 1")
  1.1086    case True
  1.1087    hence "real (x - 1) < 1" and "real x < 2" by auto
  1.1088 -  have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` by auto
  1.1089 -  hence "0 \<le> real (x - 1)" using `1 \<le> x` by auto
  1.1090 +  have "\<not> x \<le> 0" and "\<not> x < 1" using \<open>1 \<le> x\<close> by auto
  1.1091 +  hence "0 \<le> real (x - 1)" using \<open>1 \<le> x\<close> by auto
  1.1092  
  1.1093    have [simp]: "(Float 3 (- 1)) = 3 / 2" by simp
  1.1094  
  1.1095 @@ -2056,7 +2056,7 @@
  1.1096    proof (cases "x \<le> Float 3 (- 1)")
  1.1097      case True
  1.1098      show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
  1.1099 -      using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
  1.1100 +      using ln_float_bounds[OF \<open>0 \<le> real (x - 1)\<close> \<open>real (x - 1) < 1\<close>, of prec] \<open>\<not> x \<le> 0\<close> \<open>\<not> x < 1\<close> True
  1.1101        by (auto intro!: float_round_down_le float_round_up_le)
  1.1102    next
  1.1103      case False hence *: "3 / 2 < x" by auto
  1.1104 @@ -2085,7 +2085,7 @@
  1.1105        qed
  1.1106        also have "\<dots> \<le> ?ub_horner (x * rapprox_rat prec 2 3 - 1)"
  1.1107        proof (rule float_round_up_le, rule ln_float_bounds(2))
  1.1108 -        from mult_less_le_imp_less[OF `real x < 2` up] low *
  1.1109 +        from mult_less_le_imp_less[OF \<open>real x < 2\<close> up] low *
  1.1110          show "real (x * rapprox_rat prec 2 3 - 1) < 1" by auto
  1.1111          show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
  1.1112        qed
  1.1113 @@ -2107,7 +2107,7 @@
  1.1114        have "?lb_horner ?max
  1.1115          \<le> ln (real ?max + 1)"
  1.1116        proof (rule float_round_down_le, rule ln_float_bounds(1))
  1.1117 -        from mult_less_le_imp_less[OF `real x < 2` up] * low
  1.1118 +        from mult_less_le_imp_less[OF \<open>real x < 2\<close> up] * low
  1.1119          show "real ?max < 1" by (cases "real (lapprox_rat prec 2 3) = 0",
  1.1120            auto simp add: real_of_float_max)
  1.1121          show "0 \<le> real ?max" by (auto simp add: real_of_float_max)
  1.1122 @@ -2127,12 +2127,12 @@
  1.1123      }
  1.1124      ultimately
  1.1125      show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
  1.1126 -      using `\<not> x \<le> 0` `\<not> x < 1` True False by auto
  1.1127 +      using \<open>\<not> x \<le> 0\<close> \<open>\<not> x < 1\<close> True False by auto
  1.1128    qed
  1.1129  next
  1.1130    case False
  1.1131    hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 (- 1)"
  1.1132 -    using `1 \<le> x` by auto
  1.1133 +    using \<open>1 \<le> x\<close> by auto
  1.1134    show ?thesis
  1.1135    proof -
  1.1136      def m \<equiv> "mantissa x"
  1.1137 @@ -2141,12 +2141,12 @@
  1.1138      let ?s = "Float (e + (bitlen m - 1)) 0"
  1.1139      let ?x = "Float m (- (bitlen m - 1))"
  1.1140  
  1.1141 -    have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e] 
  1.1142 +    have "0 < m" and "m \<noteq> 0" using \<open>0 < x\<close> Float powr_gt_zero[of 2 e] 
  1.1143        apply (auto simp add: zero_less_mult_iff)
  1.1144        using not_le powr_ge_pzero by blast
  1.1145 -    def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using `m > 0` by (simp add: bitlen_def)
  1.1146 -    have "1 \<le> Float m e" using `1 \<le> x` Float unfolding less_eq_float_def by auto
  1.1147 -    from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \<le> Float m e`] `bl \<ge> 0`
  1.1148 +    def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using \<open>m > 0\<close> by (simp add: bitlen_def)
  1.1149 +    have "1 \<le> Float m e" using \<open>1 \<le> x\<close> Float unfolding less_eq_float_def by auto
  1.1150 +    from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
  1.1151      have x_bnds: "0 \<le> real (?x - 1)" "real (?x - 1) < 1"
  1.1152        unfolding bl_def[symmetric]
  1.1153        by (auto simp: powr_realpow[symmetric] field_simps inverse_eq_divide)
  1.1154 @@ -2158,7 +2158,7 @@
  1.1155          unfolding nat_0 power_0 mult_1_right times_float.rep_eq
  1.1156          using lb_ln2[of prec]
  1.1157        proof (rule mult_mono)
  1.1158 -        from float_gt1_scale[OF `1 \<le> Float m e`]
  1.1159 +        from float_gt1_scale[OF \<open>1 \<le> Float m e\<close>]
  1.1160          show "0 \<le> real (Float (e + (bitlen m - 1)) 0)" by simp
  1.1161        qed auto
  1.1162        moreover
  1.1163 @@ -2166,7 +2166,7 @@
  1.1164        have "float_round_down prec ((?x - 1) * lb_ln_horner prec (get_even prec) 1 (?x - 1)) \<le> ln ?x" (is "real ?lb_horner \<le> _")
  1.1165          by (auto intro!: float_round_down_le)
  1.1166        ultimately have "float_plus_down prec ?lb2 ?lb_horner \<le> ln x"
  1.1167 -        unfolding Float ln_shifted_float[OF `0 < m`, of e] by (auto intro!: float_plus_down_le)
  1.1168 +        unfolding Float ln_shifted_float[OF \<open>0 < m\<close>, of e] by (auto intro!: float_plus_down_le)
  1.1169      }
  1.1170      moreover
  1.1171      {
  1.1172 @@ -2179,18 +2179,18 @@
  1.1173          unfolding nat_0 power_0 mult_1_right times_float.rep_eq
  1.1174          using ub_ln2[of prec]
  1.1175        proof (rule mult_mono)
  1.1176 -        from float_gt1_scale[OF `1 \<le> Float m e`]
  1.1177 +        from float_gt1_scale[OF \<open>1 \<le> Float m e\<close>]
  1.1178          show "0 \<le> real (e + (bitlen m - 1))" by auto
  1.1179        next
  1.1180          have "0 \<le> ln (2 :: real)" by simp
  1.1181          thus "0 \<le> real (ub_ln2 prec)" using ub_ln2[of prec] by arith
  1.1182        qed auto
  1.1183        ultimately have "ln x \<le> float_plus_up prec ?ub2 ?ub_horner"
  1.1184 -        unfolding Float ln_shifted_float[OF `0 < m`, of e]
  1.1185 +        unfolding Float ln_shifted_float[OF \<open>0 < m\<close>, of e]
  1.1186          by (auto intro!: float_plus_up_le)
  1.1187      }
  1.1188      ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
  1.1189 -      unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 (- 1)`] Let_def
  1.1190 +      unfolding if_not_P[OF \<open>\<not> x \<le> 0\<close>] if_not_P[OF \<open>\<not> x < 1\<close>] if_not_P[OF False] if_not_P[OF \<open>\<not> x \<le> Float 3 (- 1)\<close>] Let_def
  1.1191        unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
  1.1192    qed
  1.1193  qed
  1.1194 @@ -2201,35 +2201,35 @@
  1.1195    (is "?lb \<le> ?ln \<and> ?ln \<le> ?ub")
  1.1196  proof (cases "x < 1")
  1.1197    case False hence "1 \<le> x" unfolding less_float_def less_eq_float_def by auto
  1.1198 -  show ?thesis using ub_ln_lb_ln_bounds'[OF `1 \<le> x`] .
  1.1199 +  show ?thesis using ub_ln_lb_ln_bounds'[OF \<open>1 \<le> x\<close>] .
  1.1200  next
  1.1201 -  case True have "\<not> x \<le> 0" using `0 < x` by auto
  1.1202 +  case True have "\<not> x \<le> 0" using \<open>0 < x\<close> by auto
  1.1203    from True have "real x \<le> 1" "x \<le> 1" by simp_all
  1.1204 -  have "0 < real x" and "real x \<noteq> 0" using `0 < x` by auto
  1.1205 +  have "0 < real x" and "real x \<noteq> 0" using \<open>0 < x\<close> by auto
  1.1206    hence A: "0 < 1 / real x" by auto
  1.1207  
  1.1208    {
  1.1209      let ?divl = "float_divl (max prec 1) 1 x"
  1.1210 -    have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x \<le> 1`] by auto
  1.1211 +    have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF \<open>0 < real x\<close> \<open>real x \<le> 1\<close>] by auto
  1.1212      hence B: "0 < real ?divl" by auto
  1.1213  
  1.1214      have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
  1.1215 -    hence "ln x \<le> - ln ?divl" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
  1.1216 +    hence "ln x \<le> - ln ?divl" unfolding nonzero_inverse_eq_divide[OF \<open>real x \<noteq> 0\<close>, symmetric] ln_inverse[OF \<open>0 < real x\<close>] by auto
  1.1217      from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
  1.1218      have "?ln \<le> - the (lb_ln prec ?divl)" unfolding uminus_float.rep_eq by (rule order_trans)
  1.1219    } moreover
  1.1220    {
  1.1221      let ?divr = "float_divr prec 1 x"
  1.1222 -    have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF `0 < x` `x \<le> 1`] unfolding less_eq_float_def less_float_def by auto
  1.1223 +    have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF \<open>0 < x\<close> \<open>x \<le> 1\<close>] unfolding less_eq_float_def less_float_def by auto
  1.1224      hence B: "0 < real ?divr" by auto
  1.1225  
  1.1226      have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
  1.1227 -    hence "- ln ?divr \<le> ln x" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
  1.1228 +    hence "- ln ?divr \<le> ln x" unfolding nonzero_inverse_eq_divide[OF \<open>real x \<noteq> 0\<close>, symmetric] ln_inverse[OF \<open>0 < real x\<close>] by auto
  1.1229      from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this
  1.1230      have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding uminus_float.rep_eq by (rule order_trans)
  1.1231    }
  1.1232    ultimately show ?thesis unfolding lb_ln.simps[where x=x]  ub_ln.simps[where x=x]
  1.1233 -    unfolding if_not_P[OF `\<not> x \<le> 0`] if_P[OF True] by auto
  1.1234 +    unfolding if_not_P[OF \<open>\<not> x \<le> 0\<close>] if_P[OF True] by auto
  1.1235  qed
  1.1236  
  1.1237  lemma lb_ln:
  1.1238 @@ -2242,7 +2242,7 @@
  1.1239      thus False using assms by auto
  1.1240    qed
  1.1241    thus "0 < real x" by auto
  1.1242 -  have "the (lb_ln prec x) \<le> ln x" using ub_ln_lb_ln_bounds[OF `0 < x`] ..
  1.1243 +  have "the (lb_ln prec x) \<le> ln x" using ub_ln_lb_ln_bounds[OF \<open>0 < x\<close>] ..
  1.1244    thus "y \<le> ln x" unfolding assms[symmetric] by auto
  1.1245  qed
  1.1246  
  1.1247 @@ -2256,7 +2256,7 @@
  1.1248      thus False using assms by auto
  1.1249    qed
  1.1250    thus "0 < real x" by auto
  1.1251 -  have "ln x \<le> the (ub_ln prec x)" using ub_ln_lb_ln_bounds[OF `0 < x`] ..
  1.1252 +  have "ln x \<le> the (ub_ln prec x)" using ub_ln_lb_ln_bounds[OF \<open>0 < x\<close>] ..
  1.1253    thus "ln x \<le> y" unfolding assms[symmetric] by auto
  1.1254  qed
  1.1255  
  1.1256 @@ -2269,10 +2269,10 @@
  1.1257    have "ln ux \<le> u" and "0 < real ux" using ub_ln u by auto
  1.1258    have "l \<le> ln lx" and "0 < real lx" and "0 < x" using lb_ln[OF l] x by auto
  1.1259  
  1.1260 -  from ln_le_cancel_iff[OF `0 < real lx` `0 < x`] `l \<le> ln lx`
  1.1261 +  from ln_le_cancel_iff[OF \<open>0 < real lx\<close> \<open>0 < x\<close>] \<open>l \<le> ln lx\<close>
  1.1262    have "l \<le> ln x" using x unfolding atLeastAtMost_iff by auto
  1.1263    moreover
  1.1264 -  from ln_le_cancel_iff[OF `0 < x` `0 < real ux`] `ln ux \<le> real u`
  1.1265 +  from ln_le_cancel_iff[OF \<open>0 < x\<close> \<open>0 < real ux\<close>] \<open>ln ux \<le> real u\<close>
  1.1266    have "ln x \<le> u" using x unfolding atLeastAtMost_iff by auto
  1.1267    ultimately show "l \<le> ln x \<and> ln x \<le> u" ..
  1.1268  qed
  1.1269 @@ -2387,10 +2387,10 @@
  1.1270      thus ?thesis
  1.1271      proof (cases "i = j")
  1.1272        case True
  1.1273 -      thus ?thesis using `?vs ! j = Some b` and bnd by auto
  1.1274 +      thus ?thesis using \<open>?vs ! j = Some b\<close> and bnd by auto
  1.1275      next
  1.1276        case False
  1.1277 -      thus ?thesis using `bounded_by xs vs` unfolding bounded_by_def by auto
  1.1278 +      thus ?thesis using \<open>bounded_by xs vs\<close> unfolding bounded_by_def by auto
  1.1279      qed
  1.1280    qed auto }
  1.1281    thus ?thesis unfolding bounded_by_def by auto
  1.1282 @@ -2445,7 +2445,7 @@
  1.1283      case (Some b')
  1.1284      obtain la ua where a': "a' = (la, ua)" by (cases a', auto)
  1.1285      obtain lb ub where b': "b' = (lb, ub)" by (cases b', auto)
  1.1286 -    thus ?thesis unfolding `a = Some a'` `b = Some b'` a' b' by auto
  1.1287 +    thus ?thesis unfolding \<open>a = Some a'\<close> \<open>b = Some b'\<close> a' b' by auto
  1.1288    qed
  1.1289  qed
  1.1290  
  1.1291 @@ -2503,7 +2503,7 @@
  1.1292  next
  1.1293    case (Some a')
  1.1294    obtain la ua where a': "a' = (la, ua)" by (cases a', auto)
  1.1295 -  thus ?thesis unfolding `a = Some a'` a' by auto
  1.1296 +  thus ?thesis unfolding \<open>a = Some a'\<close> a' by auto
  1.1297  qed
  1.1298  
  1.1299  lemma lift_un'_f:
  1.1300 @@ -2551,7 +2551,7 @@
  1.1301  next
  1.1302    case (Some a')
  1.1303    obtain la ua where a': "a' = (la, ua)" by (cases a', auto)
  1.1304 -  thus ?thesis unfolding `a = Some a'` a' by auto
  1.1305 +  thus ?thesis unfolding \<open>a = Some a'\<close> a' by auto
  1.1306  qed
  1.1307  
  1.1308  lemma lift_un_f:
  1.1309 @@ -2611,7 +2611,7 @@
  1.1310    assumes "bounded_by xs vs"
  1.1311    and "Some (l, u) = approx prec arith vs" (is "_ = ?g arith")
  1.1312    shows "l \<le> interpret_floatarith arith xs \<and> interpret_floatarith arith xs \<le> u" (is "?P l u arith")
  1.1313 -  using `Some (l, u) = approx prec arith vs`
  1.1314 +  using \<open>Some (l, u) = approx prec arith vs\<close>
  1.1315  proof (induct arith arbitrary: l u)
  1.1316    case (Add a b)
  1.1317    from lift_bin'[OF Add.prems[unfolded approx.simps]] Add.hyps
  1.1318 @@ -2657,26 +2657,26 @@
  1.1319      case True hence "0 < real u1" and "0 < real l1" "0 < interpret_floatarith a xs"
  1.1320        using l1_le_u1 l1 by auto
  1.1321      show ?thesis
  1.1322 -      unfolding inverse_le_iff_le[OF `0 < real u1` `0 < interpret_floatarith a xs`]
  1.1323 -        inverse_le_iff_le[OF `0 < interpret_floatarith a xs` `0 < real l1`]
  1.1324 +      unfolding inverse_le_iff_le[OF \<open>0 < real u1\<close> \<open>0 < interpret_floatarith a xs\<close>]
  1.1325 +        inverse_le_iff_le[OF \<open>0 < interpret_floatarith a xs\<close> \<open>0 < real l1\<close>]
  1.1326        using l1 u1 by auto
  1.1327    next
  1.1328      case False hence "u1 < 0" using either by blast
  1.1329      hence "real u1 < 0" and "real l1 < 0" "interpret_floatarith a xs < 0"
  1.1330        using l1_le_u1 u1 by auto
  1.1331      show ?thesis
  1.1332 -      unfolding inverse_le_iff_le_neg[OF `real u1 < 0` `interpret_floatarith a xs < 0`]
  1.1333 -        inverse_le_iff_le_neg[OF `interpret_floatarith a xs < 0` `real l1 < 0`]
  1.1334 +      unfolding inverse_le_iff_le_neg[OF \<open>real u1 < 0\<close> \<open>interpret_floatarith a xs < 0\<close>]
  1.1335 +        inverse_le_iff_le_neg[OF \<open>interpret_floatarith a xs < 0\<close> \<open>real l1 < 0\<close>]
  1.1336        using l1 u1 by auto
  1.1337    qed
  1.1338  
  1.1339    from l' have "l = float_divl prec 1 u1" by (cases "0 < l1 \<or> u1 < 0", auto)
  1.1340 -  hence "l \<le> inverse u1" unfolding nonzero_inverse_eq_divide[OF `real u1 \<noteq> 0`] using float_divl[of prec 1 u1] by auto
  1.1341 +  hence "l \<le> inverse u1" unfolding nonzero_inverse_eq_divide[OF \<open>real u1 \<noteq> 0\<close>] using float_divl[of prec 1 u1] by auto
  1.1342    also have "\<dots> \<le> inverse (interpret_floatarith a xs)" using inv by auto
  1.1343    finally have "l \<le> inverse (interpret_floatarith a xs)" .
  1.1344    moreover
  1.1345    from u' have "u = float_divr prec 1 l1" by (cases "0 < l1 \<or> u1 < 0", auto)
  1.1346 -  hence "inverse l1 \<le> u" unfolding nonzero_inverse_eq_divide[OF `real l1 \<noteq> 0`] using float_divr[of 1 l1 prec] by auto
  1.1347 +  hence "inverse l1 \<le> u" unfolding nonzero_inverse_eq_divide[OF \<open>real l1 \<noteq> 0\<close>] using float_divr[of 1 l1 prec] by auto
  1.1348    hence "inverse (interpret_floatarith a xs) \<le> u" by (rule order_trans[OF inv[THEN conjunct2]])
  1.1349    ultimately show ?case unfolding interpret_floatarith.simps using l1 u1 by auto
  1.1350  next
  1.1351 @@ -2709,7 +2709,7 @@
  1.1352  next case (Num f) thus ?case by auto
  1.1353  next
  1.1354    case (Var n)
  1.1355 -  from this[symmetric] `bounded_by xs vs`[THEN bounded_byE, of n]
  1.1356 +  from this[symmetric] \<open>bounded_by xs vs\<close>[THEN bounded_byE, of n]
  1.1357    show ?case by (cases "n < length vs", auto)
  1.1358  qed
  1.1359  
  1.1360 @@ -2776,7 +2776,7 @@
  1.1361    have "real l \<le> ?m" and "?m \<le> real u"
  1.1362      unfolding less_eq_float_def using Suc.prems by auto
  1.1363  
  1.1364 -  with `x \<in> { l .. u }`
  1.1365 +  with \<open>x \<in> { l .. u }\<close>
  1.1366    have "x \<in> { l .. ?m} \<or> x \<in> { ?m .. u }" by auto
  1.1367    thus thesis
  1.1368    proof (rule disjE)
  1.1369 @@ -2813,7 +2813,7 @@
  1.1370      obtain lx ux where bnds: "xs ! n \<in> { lx .. ux }"
  1.1371        and approx_form: "approx_form prec f (vs[n := Some (lx, ux)]) ss" .
  1.1372  
  1.1373 -    from `bounded_by xs vs` bnds
  1.1374 +    from \<open>bounded_by xs vs\<close> bnds
  1.1375      have "bounded_by xs (vs[n := Some (lx, ux)])" by (rule bounded_by_update)
  1.1376      with Bound.hyps[OF approx_form]
  1.1377      have "interpret_form f xs" by blast }
  1.1378 @@ -2836,7 +2836,7 @@
  1.1379      obtain lx ux where bnds: "xs ! n \<in> { lx .. ux }"
  1.1380        and approx_form: "approx_form prec f (vs[n := Some (lx, ux)]) ss" .
  1.1381  
  1.1382 -    from `bounded_by xs vs` bnds
  1.1383 +    from \<open>bounded_by xs vs\<close> bnds
  1.1384      have "bounded_by xs (vs[n := Some (lx, ux)])" by (rule bounded_by_update)
  1.1385      with Assign.hyps[OF approx_form]
  1.1386      have "interpret_form f xs" by blast }
  1.1387 @@ -2884,7 +2884,7 @@
  1.1388    shows "interpret_form f xs"
  1.1389    using approx_form_aux[OF _ bounded_by_None] assms by auto
  1.1390  
  1.1391 -subsection {* Implementing Taylor series expansion *}
  1.1392 +subsection \<open>Implementing Taylor series expansion\<close>
  1.1393  
  1.1394  fun isDERIV :: "nat \<Rightarrow> floatarith \<Rightarrow> real list \<Rightarrow> bool" where
  1.1395  "isDERIV x (Add a b) vs         = (isDERIV x a vs \<and> isDERIV x b vs)" |
  1.1396 @@ -2950,7 +2950,7 @@
  1.1397    thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse)
  1.1398  next
  1.1399    case (Var i)
  1.1400 -  thus ?case using `n < length vs` by auto
  1.1401 +  thus ?case using \<open>n < length vs\<close> by auto
  1.1402  qed (auto intro!: derivative_eq_intros)
  1.1403  
  1.1404  declare approx.simps[simp del]
  1.1405 @@ -2987,7 +2987,7 @@
  1.1406    then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
  1.1407      and *: "0 < l \<or> u < 0"
  1.1408      by (cases "approx prec a vs") auto
  1.1409 -  with approx[OF `bounded_by xs vs` approx_Some]
  1.1410 +  with approx[OF \<open>bounded_by xs vs\<close> approx_Some]
  1.1411    have "interpret_floatarith a xs \<noteq> 0" by auto
  1.1412    thus ?case using Inverse by auto
  1.1413  next
  1.1414 @@ -2995,7 +2995,7 @@
  1.1415    then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
  1.1416      and *: "0 < l"
  1.1417      by (cases "approx prec a vs") auto
  1.1418 -  with approx[OF `bounded_by xs vs` approx_Some]
  1.1419 +  with approx[OF \<open>bounded_by xs vs\<close> approx_Some]
  1.1420    have "0 < interpret_floatarith a xs" by auto
  1.1421    thus ?case using Ln by auto
  1.1422  next
  1.1423 @@ -3003,7 +3003,7 @@
  1.1424    then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
  1.1425      and *: "0 < l"
  1.1426      by (cases "approx prec a vs") auto
  1.1427 -  with approx[OF `bounded_by xs vs` approx_Some]
  1.1428 +  with approx[OF \<open>bounded_by xs vs\<close> approx_Some]
  1.1429    have "0 < interpret_floatarith a xs" by auto
  1.1430    thus ?case using Sqrt by auto
  1.1431  next
  1.1432 @@ -3016,7 +3016,7 @@
  1.1433    shows "bounded_by (xs[i := x]) vs"
  1.1434  proof (cases "i < length xs")
  1.1435    case False
  1.1436 -  thus ?thesis using `bounded_by xs vs` by auto
  1.1437 +  thus ?thesis using \<open>bounded_by xs vs\<close> by auto
  1.1438  next
  1.1439    let ?xs = "xs[i := x]"
  1.1440    case True hence "i < length ?xs" by auto
  1.1441 @@ -3029,12 +3029,12 @@
  1.1442        thus ?thesis
  1.1443        proof (cases "i = j")
  1.1444          case True
  1.1445 -        thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
  1.1446 +        thus ?thesis using \<open>vs ! i = Some (l, u)\<close> Some and bnd \<open>i < length ?xs\<close>
  1.1447            by auto
  1.1448        next
  1.1449          case False
  1.1450          thus ?thesis
  1.1451 -          using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some by auto
  1.1452 +          using \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>j < length vs\<close>] Some by auto
  1.1453        qed
  1.1454      qed auto
  1.1455    }
  1.1456 @@ -3047,7 +3047,7 @@
  1.1457      and approx: "isDERIV_approx prec x f vs"
  1.1458    shows "isDERIV x f (xs[x := X])"
  1.1459  proof -
  1.1460 -  note bounded_by_update_var[OF `bounded_by xs vs` vs_x X_in] approx
  1.1461 +  note bounded_by_update_var[OF \<open>bounded_by xs vs\<close> vs_x X_in] approx
  1.1462    thus ?thesis by (rule isDERIV_approx)
  1.1463  qed
  1.1464  
  1.1465 @@ -3062,8 +3062,8 @@
  1.1466    let "?i f x" = "interpret_floatarith f (xs[n := x])"
  1.1467    from approx[OF bnd app]
  1.1468    show "l \<le> ?i ?D (xs!n)" and "?i ?D (xs!n) \<le> u"
  1.1469 -    using `n < length xs` by auto
  1.1470 -  from DERIV_floatarith[OF `n < length xs`, of f "xs!n"] isDERIV_approx[OF bnd isD]
  1.1471 +    using \<open>n < length xs\<close> by auto
  1.1472 +  from DERIV_floatarith[OF \<open>n < length xs\<close>, of f "xs!n"] isDERIV_approx[OF bnd isD]
  1.1473    show "DERIV (?i f) (xs!n) :> (?i ?D (xs!n))" by simp
  1.1474  qed
  1.1475  
  1.1476 @@ -3131,7 +3131,7 @@
  1.1477    case 0
  1.1478    {
  1.1479      fix t::real assume "t \<in> {lx .. ux}"
  1.1480 -    note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
  1.1481 +    note bounded_by_update_var[OF \<open>bounded_by xs vs\<close> bnd_x this]
  1.1482      from approx[OF this 0[unfolded approx_tse.simps]]
  1.1483      have "(interpret_floatarith f (xs[x := t])) \<in> {l .. u}"
  1.1484        by (auto simp add: algebra_simps)
  1.1485 @@ -3145,7 +3145,7 @@
  1.1486      note ap = Suc.prems[unfolded approx_tse.simps if_not_P[OF False]]
  1.1487      {
  1.1488        fix t::real assume "t \<in> {lx .. ux}"
  1.1489 -      note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
  1.1490 +      note bounded_by_update_var[OF \<open>bounded_by xs vs\<close> bnd_x this]
  1.1491        from approx[OF this ap]
  1.1492        have "(interpret_floatarith f (xs[x := t])) \<in> {l .. u}"
  1.1493          by (auto simp add: algebra_simps)
  1.1494 @@ -3164,7 +3164,7 @@
  1.1495                             (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
  1.1496        by (auto elim!: lift_bin)
  1.1497  
  1.1498 -    from bnd_c `x < length xs`
  1.1499 +    from bnd_c \<open>x < length xs\<close>
  1.1500      have bnd: "bounded_by (xs[x:=c]) (vs[x:= Some (c,c)])"
  1.1501        by (auto intro!: bounded_by_update)
  1.1502  
  1.1503 @@ -3193,11 +3193,11 @@
  1.1504        have "DERIV (?f m) z :> ?f (Suc m) z"
  1.1505        proof (cases m)
  1.1506          case 0
  1.1507 -        with DERIV_floatarith[OF `x < length xs` isDERIV_approx'[OF `bounded_by xs vs` bnd_x bnd_z True]]
  1.1508 +        with DERIV_floatarith[OF \<open>x < length xs\<close> isDERIV_approx'[OF \<open>bounded_by xs vs\<close> bnd_x bnd_z True]]
  1.1509          show ?thesis by simp
  1.1510        next
  1.1511          case (Suc m')
  1.1512 -        hence "m' < n" using `m < Suc n` by auto
  1.1513 +        hence "m' < n" using \<open>m < Suc n\<close> by auto
  1.1514          from DERIV_hyp[OF this bnd_z]
  1.1515          show ?thesis using Suc by simp
  1.1516        qed
  1.1517 @@ -3213,7 +3213,7 @@
  1.1518      {
  1.1519        fix t::real assume t: "t \<in> {lx .. ux}"
  1.1520        hence "bounded_by [xs!x] [vs!x]"
  1.1521 -        using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
  1.1522 +        using \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>]
  1.1523          by (cases "vs!x", auto simp add: bounded_by_def)
  1.1524  
  1.1525        with hyp[THEN bspec, OF t] f_c
  1.1526 @@ -3249,10 +3249,10 @@
  1.1527    hence F0: "F 0 = (\<lambda> z. interpret_floatarith f (xs[x := z]))" by auto
  1.1528  
  1.1529    hence "bounded_by (xs[x := c]) vs" and "x < length vs" "x < length xs"
  1.1530 -    using `bounded_by xs vs` bnd_x bnd_c `x < length vs` `x < length xs`
  1.1531 +    using \<open>bounded_by xs vs\<close> bnd_x bnd_c \<open>x < length vs\<close> \<open>x < length xs\<close>
  1.1532      by (auto intro!: bounded_by_update_var)
  1.1533  
  1.1534 -  from approx_tse_generic[OF `bounded_by xs vs` this bnd_x ate]
  1.1535 +  from approx_tse_generic[OF \<open>bounded_by xs vs\<close> this bnd_x ate]
  1.1536    obtain n
  1.1537      where DERIV: "\<forall> m z. m < n \<and> real lx \<le> z \<and> z \<le> real ux \<longrightarrow> DERIV (F m) z :> F (Suc m) z"
  1.1538      and hyp: "\<And> (t::real). t \<in> {lx .. ux} \<Longrightarrow>
  1.1539 @@ -3263,7 +3263,7 @@
  1.1540      by blast
  1.1541  
  1.1542    have bnd_xs: "xs ! x \<in> { lx .. ux }"
  1.1543 -    using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
  1.1544 +    using \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto
  1.1545  
  1.1546    show ?thesis
  1.1547    proof (cases n)
  1.1548 @@ -3279,7 +3279,7 @@
  1.1549        case False
  1.1550  
  1.1551        have "lx \<le> real c" "real c \<le> ux" "lx \<le> xs!x" "xs!x \<le> ux"
  1.1552 -        using Suc bnd_c `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
  1.1553 +        using Suc bnd_c \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto
  1.1554        from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
  1.1555        obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
  1.1556          and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
  1.1557 @@ -3329,7 +3329,7 @@
  1.1558    have m_l: "real l \<le> ?m" and m_u: "?m \<le> real u"
  1.1559      unfolding less_eq_float_def using Suc.prems by auto
  1.1560  
  1.1561 -  with `x \<in> { l .. u }`
  1.1562 +  with \<open>x \<in> { l .. u }\<close>
  1.1563    have "x \<in> { l .. ?m} \<or> x \<in> { ?m .. u }" by auto
  1.1564    thus ?case
  1.1565    proof (rule disjE)
  1.1566 @@ -3367,7 +3367,7 @@
  1.1567    from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
  1.1568    have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
  1.1569      by auto
  1.1570 -  from order_less_le_trans[OF _ this, of 0] `0 < ly`
  1.1571 +  from order_less_le_trans[OF _ this, of 0] \<open>0 < ly\<close>
  1.1572    show ?thesis by auto
  1.1573  qed
  1.1574  
  1.1575 @@ -3389,7 +3389,7 @@
  1.1576    from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
  1.1577    have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
  1.1578      by auto
  1.1579 -  from order_trans[OF _ this, of 0] `0 \<le> ly`
  1.1580 +  from order_trans[OF _ this, of 0] \<open>0 \<le> ly\<close>
  1.1581    show ?thesis by auto
  1.1582  qed
  1.1583  
  1.1584 @@ -3462,7 +3462,7 @@
  1.1585    } thus ?thesis unfolding f_def by auto
  1.1586  qed (insert assms, auto simp add: approx_tse_form_def)
  1.1587  
  1.1588 -text {* @{term approx_form_eval} is only used for the {\tt value}-command. *}
  1.1589 +text \<open>@{term approx_form_eval} is only used for the {\tt value}-command.\<close>
  1.1590  
  1.1591  fun approx_form_eval :: "nat \<Rightarrow> form \<Rightarrow> (float * float) option list \<Rightarrow> (float * float) option list" where
  1.1592  "approx_form_eval prec (Bound (Var n) a b f) bs =
  1.1593 @@ -3479,13 +3479,13 @@
  1.1594     bs @ [approx prec x bs, approx prec a bs, approx prec b bs]" |
  1.1595  "approx_form_eval _ _ bs = bs"
  1.1596  
  1.1597 -subsection {* Implement proof method \texttt{approximation} *}
  1.1598 +subsection \<open>Implement proof method \texttt{approximation}\<close>
  1.1599  
  1.1600  lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
  1.1601    interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
  1.1602    interpret_floatarith_sin
  1.1603  
  1.1604 -oracle approximation_oracle = {* fn (thy, t) =>
  1.1605 +oracle approximation_oracle = \<open>fn (thy, t) =>
  1.1606  let
  1.1607    fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
  1.1608  
  1.1609 @@ -3582,7 +3582,7 @@
  1.1610    val normalize = eval o Envir.beta_norm o Envir.eta_long [];
  1.1611  
  1.1612  in Thm.global_cterm_of thy (Logic.mk_equals (t, normalize t)) end
  1.1613 -*}
  1.1614 +\<close>
  1.1615  
  1.1616  lemma intervalE: "a \<le> x \<and> x \<le> b \<Longrightarrow> \<lbrakk> x \<in> { a .. b } \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
  1.1617    by auto
  1.1618 @@ -3592,7 +3592,7 @@
  1.1619  
  1.1620  ML_file "approximation.ML"
  1.1621  
  1.1622 -method_setup approximation = {*
  1.1623 +method_setup approximation = \<open>
  1.1624    let val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) =>
  1.1625                     error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
  1.1626    in
  1.1627 @@ -3607,7 +3607,7 @@
  1.1628      (fn ((prec, splitting), taylor) => fn ctxt =>
  1.1629        SIMPLE_METHOD' (Approximation.approximation_tac prec splitting taylor ctxt))
  1.1630    end
  1.1631 -*} "real number approximation"
  1.1632 +\<close> "real number approximation"
  1.1633  
  1.1634  
  1.1635  section "Quickcheck Generator"
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sat Jun 20 16:23:56 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sat Jun 20 16:31:44 2015 +0200
     2.3 @@ -3,13 +3,13 @@
     2.4  Proving equalities in commutative rings done "right" in Isabelle/HOL.
     2.5  *)
     2.6  
     2.7 -section {* Proving equalities in commutative rings *}
     2.8 +section \<open>Proving equalities in commutative rings\<close>
     2.9  
    2.10  theory Commutative_Ring
    2.11  imports Main
    2.12  begin
    2.13  
    2.14 -text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
    2.15 +text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
    2.16  
    2.17  datatype 'a pol =
    2.18      Pc 'a
    2.19 @@ -24,7 +24,7 @@
    2.20    | Pow "'a polex" nat
    2.21    | Neg "'a polex"
    2.22  
    2.23 -text {* Interpretation functions for the shadow syntax. *}
    2.24 +text \<open>Interpretation functions for the shadow syntax.\<close>
    2.25  
    2.26  primrec Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
    2.27  where
    2.28 @@ -41,7 +41,7 @@
    2.29    | "Ipolex l (Pow p n) = Ipolex l p ^ n"
    2.30    | "Ipolex l (Neg P) = - Ipolex l P"
    2.31  
    2.32 -text {* Create polynomial normalized polynomials given normalized inputs. *}
    2.33 +text \<open>Create polynomial normalized polynomials given normalized inputs.\<close>
    2.34  
    2.35  definition mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
    2.36  where
    2.37 @@ -58,7 +58,7 @@
    2.38      | Pinj j R \<Rightarrow> PX P i Q
    2.39      | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)"
    2.40  
    2.41 -text {* Defining the basic ring operations on normalized polynomials *}
    2.42 +text \<open>Defining the basic ring operations on normalized polynomials\<close>
    2.43  
    2.44  lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
    2.45    by (cases p) simp_all
    2.46 @@ -120,18 +120,18 @@
    2.47  termination by (relation "measure (\<lambda>(x, y). size x + size y)")
    2.48    (auto simp add: mkPinj_def split: pol.split)
    2.49  
    2.50 -text {* Negation*}
    2.51 +text \<open>Negation\<close>
    2.52  primrec neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
    2.53  where
    2.54    "neg (Pc c) = Pc (-c)"
    2.55  | "neg (Pinj i P) = Pinj i (neg P)"
    2.56  | "neg (PX P x Q) = PX (neg P) x (neg Q)"
    2.57  
    2.58 -text {* Substraction *}
    2.59 +text \<open>Substraction\<close>
    2.60  definition sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<ominus>" 65)
    2.61    where "sub P Q = P \<oplus> neg Q"
    2.62  
    2.63 -text {* Square for Fast Exponentation *}
    2.64 +text \<open>Square for Fast Exponentation\<close>
    2.65  primrec sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
    2.66  where
    2.67    "sqr (Pc c) = Pc (c * c)"
    2.68 @@ -139,7 +139,7 @@
    2.69  | "sqr (PX A x B) =
    2.70      mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
    2.71  
    2.72 -text {* Fast Exponentation *}
    2.73 +text \<open>Fast Exponentation\<close>
    2.74  
    2.75  fun pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
    2.76  where
    2.77 @@ -162,7 +162,7 @@
    2.78    by (erule oddE) simp
    2.79  
    2.80    
    2.81 -text {* Normalization of polynomial expressions *}
    2.82 +text \<open>Normalization of polynomial expressions\<close>
    2.83  
    2.84  primrec norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
    2.85  where
    2.86 @@ -173,21 +173,21 @@
    2.87  | "norm (Pow P n) = pow n (norm P)"
    2.88  | "norm (Neg P) = neg (norm P)"
    2.89  
    2.90 -text {* mkPinj preserve semantics *}
    2.91 +text \<open>mkPinj preserve semantics\<close>
    2.92  lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
    2.93    by (induct B) (auto simp add: mkPinj_def algebra_simps)
    2.94  
    2.95 -text {* mkPX preserves semantics *}
    2.96 +text \<open>mkPX preserves semantics\<close>
    2.97  lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
    2.98    by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
    2.99  
   2.100 -text {* Correctness theorems for the implemented operations *}
   2.101 +text \<open>Correctness theorems for the implemented operations\<close>
   2.102  
   2.103 -text {* Negation *}
   2.104 +text \<open>Negation\<close>
   2.105  lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
   2.106    by (induct P arbitrary: l) auto
   2.107  
   2.108 -text {* Addition *}
   2.109 +text \<open>Addition\<close>
   2.110  lemma add_ci: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
   2.111  proof (induct P Q arbitrary: l rule: add.induct)
   2.112    case (6 x P y Q)
   2.113 @@ -237,21 +237,21 @@
   2.114    qed
   2.115  qed (auto simp add: algebra_simps)
   2.116  
   2.117 -text {* Multiplication *}
   2.118 +text \<open>Multiplication\<close>
   2.119  lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
   2.120    by (induct P Q arbitrary: l rule: mul.induct)
   2.121      (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add)
   2.122  
   2.123 -text {* Substraction *}
   2.124 +text \<open>Substraction\<close>
   2.125  lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
   2.126    by (simp add: add_ci neg_ci sub_def)
   2.127  
   2.128 -text {* Square *}
   2.129 +text \<open>Square\<close>
   2.130  lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
   2.131    by (induct P arbitrary: ls)
   2.132      (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
   2.133  
   2.134 -text {* Power *}
   2.135 +text \<open>Power\<close>
   2.136  lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
   2.137  proof (induct n arbitrary: P rule: less_induct)
   2.138    case (less k)
   2.139 @@ -274,11 +274,11 @@
   2.140    qed
   2.141  qed
   2.142  
   2.143 -text {* Normalization preserves semantics  *}
   2.144 +text \<open>Normalization preserves semantics\<close>
   2.145  lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
   2.146    by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
   2.147  
   2.148 -text {* Reflection lemma: Key to the (incomplete) decision procedure *}
   2.149 +text \<open>Reflection lemma: Key to the (incomplete) decision procedure\<close>
   2.150  lemma norm_eq:
   2.151    assumes "norm P1 = norm P2"
   2.152    shows "Ipolex l P1 = Ipolex l P2"
   2.153 @@ -290,8 +290,8 @@
   2.154  
   2.155  ML_file "commutative_ring_tac.ML"
   2.156  
   2.157 -method_setup comm_ring = {*
   2.158 +method_setup comm_ring = \<open>
   2.159    Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
   2.160 -*} "reflective decision procedure for equalities over commutative rings"
   2.161 +\<close> "reflective decision procedure for equalities over commutative rings"
   2.162  
   2.163  end
     3.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sat Jun 20 16:23:56 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sat Jun 20 16:31:44 2015 +0200
     3.3 @@ -5,13 +5,13 @@
     3.4  in normal form, the cring method is complete.
     3.5  *)
     3.6  
     3.7 -section {* Proof of the relative completeness of method comm-ring *}
     3.8 +section \<open>Proof of the relative completeness of method comm-ring\<close>
     3.9  
    3.10  theory Commutative_Ring_Complete
    3.11  imports Commutative_Ring
    3.12  begin
    3.13  
    3.14 -text {* Formalization of normal form *}
    3.15 +text \<open>Formalization of normal form\<close>
    3.16  fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
    3.17  where
    3.18    "isnorm (Pc c) \<longleftrightarrow> True"
    3.19 @@ -101,7 +101,7 @@
    3.20      by (cases x) auto
    3.21  qed
    3.22  
    3.23 -text {* mkPX conserves normalizedness (@{text "_cn"}) *}
    3.24 +text \<open>mkPX conserves normalizedness (@{text "_cn"})\<close>
    3.25  lemma mkPX_cn:
    3.26    assumes "x \<noteq> 0"
    3.27      and "isnorm P"
    3.28 @@ -125,7 +125,7 @@
    3.29      by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
    3.30  qed
    3.31  
    3.32 -text {* add conserves normalizedness *}
    3.33 +text \<open>add conserves normalizedness\<close>
    3.34  lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
    3.35  proof (induct P Q rule: add.induct)
    3.36    case (2 c i P2)
    3.37 @@ -164,7 +164,7 @@
    3.38      from 6 have "isnorm P2" "isnorm Q2"
    3.39        by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
    3.40      moreover
    3.41 -    from 6 `x < y` y have "isnorm (Pinj d Q2)"
    3.42 +    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
    3.43        by (cases d, simp, cases Q2, auto)
    3.44      ultimately have ?case by (simp add: mkPinj_cn)
    3.45    }
    3.46 @@ -188,7 +188,7 @@
    3.47      from 6 have "isnorm P2" "isnorm Q2"
    3.48        by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
    3.49      moreover
    3.50 -    from 6 `x > y` x have "isnorm (Pinj d P2)"
    3.51 +    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
    3.52        by (cases d) (simp, cases P2, auto)
    3.53      ultimately have ?case by (simp add: mkPinj_cn)
    3.54    }
    3.55 @@ -204,8 +204,8 @@
    3.56      assume "x = 1"
    3.57      from 7 have "isnorm R" "isnorm P2"
    3.58        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
    3.59 -    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
    3.60 -    with 7 `x = 1` have ?case
    3.61 +    with 7 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)" by simp
    3.62 +    with 7 \<open>x = 1\<close> have ?case
    3.63        by (simp add: norm_PXtrans[of Q2 y _])
    3.64    }
    3.65    moreover {
    3.66 @@ -215,7 +215,7 @@
    3.67        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
    3.68      with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
    3.69      with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
    3.70 -    with `isnorm (PX Q2 y R)` X have ?case
    3.71 +    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
    3.72        by (simp add: norm_PXtrans[of Q2 y _])
    3.73    }
    3.74    ultimately show ?case by blast
    3.75 @@ -231,9 +231,9 @@
    3.76      assume "x = 1"
    3.77      with 8 have "isnorm R" "isnorm P2"
    3.78        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
    3.79 -    with 8 `x = 1` have "isnorm (R \<oplus> P2)"
    3.80 +    with 8 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)"
    3.81        by simp
    3.82 -    with 8 `x = 1` have ?case
    3.83 +    with 8 \<open>x = 1\<close> have ?case
    3.84        by (simp add: norm_PXtrans[of Q2 y _])
    3.85    }
    3.86    moreover {
    3.87 @@ -244,9 +244,9 @@
    3.88        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
    3.89      with 8 X have "isnorm (Pinj (x - 1) P2)"
    3.90        by (cases P2) auto
    3.91 -    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
    3.92 +    with 8 \<open>x > 1\<close> NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
    3.93        by simp
    3.94 -    with `isnorm (PX Q2 y R)` X have ?case
    3.95 +    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
    3.96        by (simp add: norm_PXtrans[of Q2 y _])
    3.97    }
    3.98    ultimately show ?case by blast
    3.99 @@ -288,7 +288,7 @@
   3.100      assume "x = y"
   3.101      with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
   3.102        by auto
   3.103 -    with `x = y` Y0 have ?case
   3.104 +    with \<open>x = y\<close> Y0 have ?case
   3.105        by (simp add: mkPX_cn)
   3.106    }
   3.107    moreover {
   3.108 @@ -319,7 +319,7 @@
   3.109    ultimately show ?case by blast
   3.110  qed simp
   3.111  
   3.112 -text {* mul concerves normalizedness *}
   3.113 +text \<open>mul concerves normalizedness\<close>
   3.114  lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
   3.115  proof (induct P Q rule: mul.induct)
   3.116    case (2 c i P2)
   3.117 @@ -357,7 +357,7 @@
   3.118      from 6 have "isnorm P2" "isnorm Q2"
   3.119        by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   3.120      moreover
   3.121 -    from 6 `x < y` y have "isnorm (Pinj d Q2)"
   3.122 +    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
   3.123        by (cases d) (simp, cases Q2, auto)
   3.124      ultimately have ?case by (simp add: mkPinj_cn)
   3.125    }
   3.126 @@ -386,7 +386,7 @@
   3.127      from 6 have "isnorm P2" "isnorm Q2"
   3.128        by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   3.129      moreover
   3.130 -    from 6 `x > y` x have "isnorm (Pinj d P2)"
   3.131 +    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
   3.132        by (cases d) (simp, cases P2, auto)
   3.133      ultimately have ?case by (simp add: mkPinj_cn)
   3.134    }
   3.135 @@ -404,9 +404,9 @@
   3.136      assume "x = 1"
   3.137      from 7 have "isnorm R" "isnorm P2"
   3.138        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   3.139 -    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
   3.140 +    with 7 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
   3.141        by (auto simp add: norm_PX1[of Q2 y R])
   3.142 -    with 7 `x = 1` Y0 have ?case
   3.143 +    with 7 \<open>x = 1\<close> Y0 have ?case
   3.144        by (simp add: mkPX_cn)
   3.145    }
   3.146    moreover {
   3.147 @@ -444,9 +444,9 @@
   3.148      assume "x = 1"
   3.149      from 8 have "isnorm R" "isnorm P2"
   3.150        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   3.151 -    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
   3.152 +    with 8 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
   3.153        by (auto simp add: norm_PX1[of Q2 y R])
   3.154 -    with 8 `x = 1` Y0 have ?case
   3.155 +    with 8 \<open>x = 1\<close> Y0 have ?case
   3.156        by (simp add: mkPX_cn)
   3.157    }
   3.158    moreover {
   3.159 @@ -490,7 +490,7 @@
   3.160    then show ?case by (simp add: add_cn)
   3.161  qed simp
   3.162  
   3.163 -text {* neg conserves normalizedness *}
   3.164 +text \<open>neg conserves normalizedness\<close>
   3.165  lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
   3.166  proof (induct P)
   3.167    case (Pinj i P2)
   3.168 @@ -514,11 +514,11 @@
   3.169    qed (cases x, auto)
   3.170  qed simp
   3.171  
   3.172 -text {* sub conserves normalizedness *}
   3.173 +text \<open>sub conserves normalizedness\<close>
   3.174  lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
   3.175    by (simp add: sub_def add_cn neg_cn)
   3.176  
   3.177 -text {* sqr conserves normalizizedness *}
   3.178 +text \<open>sqr conserves normalizizedness\<close>
   3.179  lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
   3.180  proof (induct P)
   3.181    case Pc
   3.182 @@ -538,7 +538,7 @@
   3.183      by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   3.184  qed
   3.185  
   3.186 -text {* pow conserves normalizedness *}
   3.187 +text \<open>pow conserves normalizedness\<close>
   3.188  lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
   3.189  proof (induct n arbitrary: P rule: less_induct)
   3.190    case (less k)
     4.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sat Jun 20 16:23:56 2015 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Jun 20 16:31:44 2015 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
     4.5    | Mul int num
     4.6  
     4.7 -primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
     4.8 +primrec num_size :: "num \<Rightarrow> nat" -- \<open>A size for num to make inductive proofs simpler\<close>
     4.9  where
    4.10    "num_size (C c) = 1"
    4.11  | "num_size (Bound n) = 1"
    4.12 @@ -44,7 +44,7 @@
    4.13    | Closed nat | NClosed nat
    4.14  
    4.15  
    4.16 -fun fmsize :: "fm \<Rightarrow> nat"  -- {* A size for fm *}
    4.17 +fun fmsize :: "fm \<Rightarrow> nat"  -- \<open>A size for fm\<close>
    4.18  where
    4.19    "fmsize (NOT p) = 1 + fmsize p"
    4.20  | "fmsize (And p q) = 1 + fmsize p + fmsize q"
    4.21 @@ -60,7 +60,7 @@
    4.22  lemma fmsize_pos: "fmsize p > 0"
    4.23    by (induct p rule: fmsize.induct) simp_all
    4.24  
    4.25 -primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
    4.26 +primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- \<open>Semantics of formulae (fm)\<close>
    4.27  where
    4.28    "Ifm bbs bs T \<longleftrightarrow> True"
    4.29  | "Ifm bbs bs F \<longleftrightarrow> False"
    4.30 @@ -113,7 +113,7 @@
    4.31    by (induct p arbitrary: bs rule: prep.induct) auto
    4.32  
    4.33  
    4.34 -fun qfree :: "fm \<Rightarrow> bool"  -- {* Quantifier freeness *}
    4.35 +fun qfree :: "fm \<Rightarrow> bool"  -- \<open>Quantifier freeness\<close>
    4.36  where
    4.37    "qfree (E p) \<longleftrightarrow> False"
    4.38  | "qfree (A p) \<longleftrightarrow> False"
    4.39 @@ -125,9 +125,9 @@
    4.40  | "qfree p \<longleftrightarrow> True"
    4.41  
    4.42  
    4.43 -text {* Boundedness and substitution *}
    4.44 +text \<open>Boundedness and substitution\<close>
    4.45  
    4.46 -primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
    4.47 +primrec numbound0 :: "num \<Rightarrow> bool"  -- \<open>a num is INDEPENDENT of Bound 0\<close>
    4.48  where
    4.49    "numbound0 (C c) \<longleftrightarrow> True"
    4.50  | "numbound0 (Bound n) \<longleftrightarrow> n > 0"
    4.51 @@ -142,7 +142,7 @@
    4.52    shows "Inum (b # bs) a = Inum (b' # bs) a"
    4.53    using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
    4.54  
    4.55 -primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
    4.56 +primrec bound0 :: "fm \<Rightarrow> bool" -- \<open>A Formula is independent of Bound 0\<close>
    4.57  where
    4.58    "bound0 T \<longleftrightarrow> True"
    4.59  | "bound0 F \<longleftrightarrow> True"
    4.60 @@ -188,7 +188,7 @@
    4.61    "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
    4.62    by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
    4.63  
    4.64 -primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- {* substitue a num into a formula for Bound 0 *}
    4.65 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- \<open>substitue a num into a formula for Bound 0\<close>
    4.66  where
    4.67    "subst0 t T = T"
    4.68  | "subst0 t F = F"
    4.69 @@ -254,7 +254,7 @@
    4.70  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
    4.71    by (induct p) simp_all
    4.72  
    4.73 -fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
    4.74 +fun isatom :: "fm \<Rightarrow> bool"  -- \<open>test for atomicity\<close>
    4.75  where
    4.76    "isatom T \<longleftrightarrow> True"
    4.77  | "isatom F \<longleftrightarrow> True"
    4.78 @@ -399,9 +399,9 @@
    4.79  qed
    4.80  
    4.81  
    4.82 -text {* Simplification *}
    4.83 +text \<open>Simplification\<close>
    4.84  
    4.85 -text {* Algebraic simplifications for nums *}
    4.86 +text \<open>Algebraic simplifications for nums\<close>
    4.87  
    4.88  fun bnds :: "num \<Rightarrow> nat list"
    4.89  where
    4.90 @@ -864,7 +864,7 @@
    4.91    by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
    4.92      (case_tac "simpnum a", auto)+
    4.93  
    4.94 -text {* Generic quantifier elimination *}
    4.95 +text \<open>Generic quantifier elimination\<close>
    4.96  function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
    4.97  where
    4.98    "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
    4.99 @@ -886,9 +886,9 @@
   4.100      (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
   4.101        simpfm simpfm_qf simp del: simpfm.simps)
   4.102  
   4.103 -text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
   4.104 +text \<open>Linearity for fm where Bound 0 ranges over @{text "\<int>"}\<close>
   4.105  
   4.106 -fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- {* splits the bounded from the unbounded part *}
   4.107 +fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- \<open>splits the bounded from the unbounded part\<close>
   4.108  where
   4.109    "zsplit0 (C c) = (0, C c)"
   4.110  | "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
   4.111 @@ -1021,7 +1021,7 @@
   4.112      by simp
   4.113  qed
   4.114  
   4.115 -consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}
   4.116 +consts iszlfm :: "fm \<Rightarrow> bool"  -- \<open>Linearity test for fm\<close>
   4.117  recdef iszlfm "measure size"
   4.118    "iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
   4.119    "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
   4.120 @@ -1038,7 +1038,7 @@
   4.121  lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
   4.122    by (induct p rule: iszlfm.induct) auto
   4.123  
   4.124 -consts zlfm :: "fm \<Rightarrow> fm"  -- {* Linearity transformation for fm *}
   4.125 +consts zlfm :: "fm \<Rightarrow> fm"  -- \<open>Linearity transformation for fm\<close>
   4.126  recdef zlfm "measure fmsize"
   4.127    "zlfm (And p q) = And (zlfm p) (zlfm q)"
   4.128    "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
   4.129 @@ -1231,7 +1231,7 @@
   4.130      assume "j = 0"
   4.131      then have z: "zlfm (Dvd j a) = (zlfm (Eq a))"
   4.132        by (simp add: Let_def)
   4.133 -    then have ?case using 11 `j = 0`
   4.134 +    then have ?case using 11 \<open>j = 0\<close>
   4.135        by (simp del: zlfm.simps)
   4.136    }
   4.137    moreover
   4.138 @@ -1282,7 +1282,7 @@
   4.139      then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
   4.140        by (simp add: Let_def)
   4.141      then have ?case
   4.142 -      using assms 12 `j = 0` by (simp del: zlfm.simps)
   4.143 +      using assms 12 \<open>j = 0\<close> by (simp del: zlfm.simps)
   4.144    }
   4.145    moreover
   4.146    {
   4.147 @@ -1316,7 +1316,7 @@
   4.148    ultimately show ?case by blast
   4.149  qed auto
   4.150  
   4.151 -consts minusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "-\<infinity>"} *}
   4.152 +consts minusinf :: "fm \<Rightarrow> fm" -- \<open>Virtual substitution of @{text "-\<infinity>"}\<close>
   4.153  recdef minusinf "measure size"
   4.154    "minusinf (And p q) = And (minusinf p) (minusinf q)"
   4.155    "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
   4.156 @@ -1331,7 +1331,7 @@
   4.157  lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
   4.158    by (induct p rule: minusinf.induct) auto
   4.159  
   4.160 -consts plusinf :: "fm \<Rightarrow> fm"  -- {* Virtual substitution of @{text "+\<infinity>"} *}
   4.161 +consts plusinf :: "fm \<Rightarrow> fm"  -- \<open>Virtual substitution of @{text "+\<infinity>"}\<close>
   4.162  recdef plusinf "measure size"
   4.163    "plusinf (And p q) = And (plusinf p) (plusinf q)"
   4.164    "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
   4.165 @@ -1343,7 +1343,7 @@
   4.166    "plusinf (Ge  (CN 0 c e)) = T"
   4.167    "plusinf p = p"
   4.168  
   4.169 -consts \<delta> :: "fm \<Rightarrow> int"  -- {* Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"} *}
   4.170 +consts \<delta> :: "fm \<Rightarrow> int"  -- \<open>Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"}\<close>
   4.171  recdef \<delta> "measure size"
   4.172    "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
   4.173    "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
   4.174 @@ -1351,7 +1351,7 @@
   4.175    "\<delta> (NDvd i (CN 0 c e)) = i"
   4.176    "\<delta> p = 1"
   4.177  
   4.178 -consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* check if a given l divides all the ds above *}
   4.179 +consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- \<open>check if a given l divides all the ds above\<close>
   4.180  recdef d_\<delta> "measure size"
   4.181    "d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
   4.182    "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
   4.183 @@ -1412,7 +1412,7 @@
   4.184  qed simp_all
   4.185  
   4.186  
   4.187 -consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- {* adjust the coefficients of a formula *}
   4.188 +consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- \<open>adjust the coefficients of a formula\<close>
   4.189  recdef a_\<beta> "measure size"
   4.190    "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
   4.191    "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
   4.192 @@ -1426,7 +1426,7 @@
   4.193    "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   4.194    "a_\<beta> p = (\<lambda>k. p)"
   4.195  
   4.196 -consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* test if all coeffs c of c divide a given l *}
   4.197 +consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- \<open>test if all coeffs c of c divide a given l\<close>
   4.198  recdef d_\<beta> "measure size"
   4.199    "d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   4.200    "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   4.201 @@ -1440,7 +1440,7 @@
   4.202    "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
   4.203    "d_\<beta> p = (\<lambda>k. True)"
   4.204  
   4.205 -consts \<zeta> :: "fm \<Rightarrow> int"  -- {* computes the lcm of all coefficients of x *}
   4.206 +consts \<zeta> :: "fm \<Rightarrow> int"  -- \<open>computes the lcm of all coefficients of x\<close>
   4.207  recdef \<zeta> "measure size"
   4.208    "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
   4.209    "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
   4.210 @@ -1492,7 +1492,7 @@
   4.211    "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   4.212    "mirror p = p"
   4.213  
   4.214 -text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
   4.215 +text \<open>Lemmas for the correctness of @{text "\<sigma>_\<rho>"}\<close>
   4.216  
   4.217  lemma dvd1_eq1:
   4.218    fixes x :: int
   4.219 @@ -2370,7 +2370,7 @@
   4.220  qed
   4.221  
   4.222  
   4.223 -text {* Cooper's Algorithm *}
   4.224 +text \<open>Cooper's Algorithm\<close>
   4.225  
   4.226  definition cooper :: "fm \<Rightarrow> fm"
   4.227  where
   4.228 @@ -2500,13 +2500,13 @@
   4.229        pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
   4.230          (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
   4.231  
   4.232 -ML_val {* @{code cooper_test} () *}
   4.233 +ML_val \<open>@{code cooper_test} ()\<close>
   4.234  
   4.235  (*code_reflect Cooper_Procedure
   4.236    functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
   4.237    file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*)
   4.238  
   4.239 -oracle linzqe_oracle = {*
   4.240 +oracle linzqe_oracle = \<open>
   4.241  let
   4.242  
   4.243  fun num_of_term vs (t as Free (xn, xT)) =
   4.244 @@ -2649,17 +2649,17 @@
   4.245        val t' = term_of_fm ps vs (@{code pa} (fm_of_term ps vs t));
   4.246      in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
   4.247  end;
   4.248 -*}
   4.249 +\<close>
   4.250  
   4.251  ML_file "cooper_tac.ML"
   4.252  
   4.253 -method_setup cooper = {*
   4.254 +method_setup cooper = \<open>
   4.255    Scan.lift (Args.mode "no_quantify") >>
   4.256      (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
   4.257 -*} "decision procedure for linear integer arithmetic"
   4.258 +\<close> "decision procedure for linear integer arithmetic"
   4.259  
   4.260  
   4.261 -text {* Tests *}
   4.262 +text \<open>Tests\<close>
   4.263  
   4.264  lemma "\<exists>(j::int). \<forall>x\<ge>j. \<exists>a b. x = 3*a+5*b"
   4.265    by cooper
     5.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat Jun 20 16:23:56 2015 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sat Jun 20 16:31:44 2015 +0200
     5.3 @@ -2,8 +2,8 @@
     5.4      Author      : Amine Chaieb, TU Muenchen
     5.5  *)
     5.6  
     5.7 -section {* Dense linear order without endpoints
     5.8 -  and a quantifier elimination procedure in Ferrante and Rackoff style *}
     5.9 +section \<open>Dense linear order without endpoints
    5.10 +  and a quantifier elimination procedure in Ferrante and Rackoff style\<close>
    5.11  
    5.12  theory Dense_Linear_Order
    5.13  imports Main
    5.14 @@ -32,7 +32,7 @@
    5.15  lemma gather_start [no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
    5.16    by simp
    5.17  
    5.18 -text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}*}
    5.19 +text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
    5.20  lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
    5.21  lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
    5.22    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    5.23 @@ -44,7 +44,7 @@
    5.24  lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    5.25  lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    5.26  
    5.27 -text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}*}
    5.28 +text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close>
    5.29  lemma pinf_gt[no_atp]:  "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
    5.30  lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
    5.31    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    5.32 @@ -239,7 +239,7 @@
    5.33  end
    5.34  
    5.35  
    5.36 -section {* The classical QE after Langford for dense linear orders *}
    5.37 +section \<open>The classical QE after Langford for dense linear orders\<close>
    5.38  
    5.39  context unbounded_dense_linorder
    5.40  begin
    5.41 @@ -324,14 +324,14 @@
    5.42  lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
    5.43  
    5.44  ML_file "langford.ML"
    5.45 -method_setup dlo = {*
    5.46 +method_setup dlo = \<open>
    5.47    Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
    5.48 -*} "Langford's algorithm for quantifier elimination in dense linear orders"
    5.49 +\<close> "Langford's algorithm for quantifier elimination in dense linear orders"
    5.50  
    5.51  
    5.52 -section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *}
    5.53 +section \<open>Contructive dense linear orders yield QE for linear arithmetic over ordered Fields\<close>
    5.54  
    5.55 -text {* Linear order without upper bounds *}
    5.56 +text \<open>Linear order without upper bounds\<close>
    5.57  
    5.58  locale linorder_stupid_syntax = linorder
    5.59  begin
    5.60 @@ -350,7 +350,7 @@
    5.61  
    5.62  lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
    5.63  
    5.64 -text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"} *}
    5.65 +text \<open>Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close>
    5.66  lemma pinf_conj[no_atp]:
    5.67    assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
    5.68    and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
    5.69 @@ -392,7 +392,7 @@
    5.70  
    5.71  end
    5.72  
    5.73 -text {* Linear order without upper bounds *}
    5.74 +text \<open>Linear order without upper bounds\<close>
    5.75  
    5.76  locale linorder_no_lb = linorder_stupid_syntax +
    5.77    assumes lt_ex: "\<exists>y. less y x"
    5.78 @@ -401,7 +401,7 @@
    5.79  lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
    5.80  
    5.81  
    5.82 -text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"} *}
    5.83 +text \<open>Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
    5.84  lemma minf_conj[no_atp]:
    5.85    assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
    5.86      and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
    5.87 @@ -551,7 +551,7 @@
    5.88      nmi: nmi_thms npi: npi_thms lindense:
    5.89      lin_dense_thms qe: fr_eq atoms: atoms]
    5.90  
    5.91 -declaration {*
    5.92 +declaration \<open>
    5.93  let
    5.94    fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
    5.95    fun generic_whatis phi =
    5.96 @@ -582,18 +582,18 @@
    5.97    Ferrante_Rackoff_Data.funs  @{thm "ferrack_axiom"}
    5.98      {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
    5.99  end
   5.100 -*}
   5.101 +\<close>
   5.102  
   5.103  end
   5.104  
   5.105  ML_file "ferrante_rackoff.ML"
   5.106  
   5.107 -method_setup ferrack = {*
   5.108 +method_setup ferrack = \<open>
   5.109    Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   5.110 -*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
   5.111 +\<close> "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
   5.112  
   5.113  
   5.114 -subsection {* Ferrante and Rackoff algorithm over ordered fields *}
   5.115 +subsection \<open>Ferrante and Rackoff algorithm over ordered fields\<close>
   5.116  
   5.117  lemma neg_prod_lt:"(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))"
   5.118  proof -
   5.119 @@ -702,7 +702,7 @@
   5.120     "\<lambda> x y. 1/2 * ((x::'a::{linordered_field}) + y)"
   5.121    by unfold_locales (dlo, dlo, auto)
   5.122  
   5.123 -declaration{*
   5.124 +declaration\<open>
   5.125  let
   5.126    fun earlier [] x y = false
   5.127      | earlier (h::t) x y =
   5.128 @@ -933,7 +933,7 @@
   5.129  Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"}
   5.130    {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
   5.131  end
   5.132 -*}
   5.133 +\<close>
   5.134  (*
   5.135  lemma upper_bound_finite_set:
   5.136    assumes fS: "finite S"
     6.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Jun 20 16:23:56 2015 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Jun 20 16:31:44 2015 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4    "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
     6.5  begin
     6.6  
     6.7 -section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}
     6.8 +section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, <)"}\<close>
     6.9  
    6.10    (*********************************************************************************)
    6.11    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    6.12 @@ -1914,9 +1914,9 @@
    6.13    "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
    6.14      (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
    6.15  
    6.16 -ML_val {* @{code ferrack_test} () *}
    6.17 +ML_val \<open>@{code ferrack_test} ()\<close>
    6.18  
    6.19 -oracle linr_oracle = {*
    6.20 +oracle linr_oracle = \<open>
    6.21  let
    6.22  
    6.23  val mk_C = @{code C} o @{code int_of_integer};
    6.24 @@ -2001,14 +2001,14 @@
    6.25      val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
    6.26    in (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
    6.27  end;
    6.28 -*}
    6.29 +\<close>
    6.30  
    6.31  ML_file "ferrack_tac.ML"
    6.32  
    6.33 -method_setup rferrack = {*
    6.34 +method_setup rferrack = \<open>
    6.35    Scan.lift (Args.mode "no_quantify") >>
    6.36      (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
    6.37 -*} "decision procedure for linear real arithmetic"
    6.38 +\<close> "decision procedure for linear real arithmetic"
    6.39  
    6.40  
    6.41  lemma
     7.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Jun 20 16:23:56 2015 +0200
     7.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Jun 20 16:31:44 2015 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4    "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
     7.5  begin
     7.6  
     7.7 -section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
     7.8 +section \<open>Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"}\<close>
     7.9  
    7.10  declare real_of_int_floor_cancel [simp del]
    7.11  
    7.12 @@ -63,7 +63,7 @@
    7.13    assume "?r" hence "(i\<Colon>int) dvd \<lfloor>x\<Colon>real\<rfloor>" ..
    7.14    hence "\<exists> k. real (floor x) = real (i*k)" 
    7.15      by (simp only: real_of_int_inject) (simp add: dvd_def)
    7.16 -  thus ?l using `?r` by (simp add: rdvd_def)
    7.17 +  thus ?l using \<open>?r\<close> by (simp add: rdvd_def)
    7.18  qed
    7.19  
    7.20  lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)"
    7.21 @@ -1450,8 +1450,8 @@
    7.22    by (induct p rule: qelim.induct) (auto simp del: simpfm.simps)
    7.23  
    7.24  
    7.25 -text {* The @{text "\<int>"} Part *}
    7.26 -text{* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
    7.27 +text \<open>The @{text "\<int>"} Part\<close>
    7.28 +text\<open>Linearity for fm where Bound 0 ranges over @{text "\<int>"}\<close>
    7.29  
    7.30  function zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*) where
    7.31    "zsplit0 (C c) = (0,C c)"
    7.32 @@ -1955,10 +1955,10 @@
    7.33    ultimately show ?case by blast
    7.34  qed auto
    7.35  
    7.36 -text{* plusinf : Virtual substitution of @{text "+\<infinity>"}
    7.37 +text\<open>plusinf : Virtual substitution of @{text "+\<infinity>"}
    7.38         minusinf: Virtual substitution of @{text "-\<infinity>"}
    7.39         @{text "\<delta>"} Compute lcm @{text "d| Dvd d  c*x+t \<in> p"}
    7.40 -       @{text "d_\<delta>"} checks if a given l divides all the ds above*}
    7.41 +       @{text "d_\<delta>"} checks if a given l divides all the ds above\<close>
    7.42  
    7.43  fun minusinf:: "fm \<Rightarrow> fm" where
    7.44    "minusinf (And p q) = conj (minusinf p) (minusinf q)" 
    7.45 @@ -3294,9 +3294,9 @@
    7.46    using lp
    7.47    by (induct p rule: mirror.induct) (simp_all add: split_def image_Un)
    7.48    
    7.49 -text {* The @{text "\<real>"} part*}
    7.50 -
    7.51 -text{* Linearity for fm where Bound 0 ranges over @{text "\<real>"}*}
    7.52 +text \<open>The @{text "\<real>"} part\<close>
    7.53 +
    7.54 +text\<open>Linearity for fm where Bound 0 ranges over @{text "\<real>"}\<close>
    7.55  consts
    7.56    isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
    7.57  recdef isrlfm "measure size"
    7.58 @@ -3983,10 +3983,10 @@
    7.59      { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
    7.60        with numgcd_pos[where t="CN 0 c (simpnum e)"]
    7.61        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
    7.62 -      from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
    7.63 +      from \<open>c > 0\<close> have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
    7.64          by (simp add: numgcd_def)
    7.65 -      from `c > 0` have th': "c\<noteq>0" by auto
    7.66 -      from `c > 0` have cp: "c \<ge> 0" by simp
    7.67 +      from \<open>c > 0\<close> have th': "c\<noteq>0" by auto
    7.68 +      from \<open>c > 0\<close> have cp: "c \<ge> 0" by simp
    7.69        from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
    7.70        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
    7.71      }
    7.72 @@ -4007,10 +4007,10 @@
    7.73      { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
    7.74        with numgcd_pos[where t="CN 0 c (simpnum e)"]
    7.75        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
    7.76 -      from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
    7.77 +      from \<open>c > 0\<close> have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
    7.78          by (simp add: numgcd_def)
    7.79 -      from `c > 0` have th': "c\<noteq>0" by auto
    7.80 -      from `c > 0` have cp: "c \<ge> 0" by simp
    7.81 +      from \<open>c > 0\<close> have th': "c\<noteq>0" by auto
    7.82 +      from \<open>c > 0\<close> have cp: "c \<ge> 0" by simp
    7.83        from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
    7.84        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
    7.85      }
    7.86 @@ -4031,10 +4031,10 @@
    7.87      { assume cn1: "numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
    7.88        with numgcd_pos[where t="CN 0 c (simpnum e)"]
    7.89        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
    7.90 -      from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
    7.91 +      from \<open>c > 0\<close> have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
    7.92          by (simp add: numgcd_def)
    7.93 -      from `c > 0` have th': "c\<noteq>0" by auto
    7.94 -      from `c > 0` have cp: "c \<ge> 0" by simp
    7.95 +      from \<open>c > 0\<close> have th': "c\<noteq>0" by auto
    7.96 +      from \<open>c > 0\<close> have cp: "c \<ge> 0" by simp
    7.97        from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
    7.98        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
    7.99      }
   7.100 @@ -4055,10 +4055,10 @@
   7.101      { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
   7.102        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   7.103        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   7.104 -      from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   7.105 +      from \<open>c > 0\<close> have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   7.106          by (simp add: numgcd_def)
   7.107 -      from `c > 0` have th': "c\<noteq>0" by auto
   7.108 -      from `c > 0` have cp: "c \<ge> 0" by simp
   7.109 +      from \<open>c > 0\<close> have th': "c\<noteq>0" by auto
   7.110 +      from \<open>c > 0\<close> have cp: "c \<ge> 0" by simp
   7.111        from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   7.112        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   7.113      }
   7.114 @@ -4079,10 +4079,10 @@
   7.115      { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
   7.116        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   7.117        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   7.118 -      from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   7.119 +      from \<open>c > 0\<close> have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   7.120          by (simp add: numgcd_def)
   7.121 -      from `c > 0` have th': "c\<noteq>0" by auto
   7.122 -      from `c > 0` have cp: "c \<ge> 0" by simp
   7.123 +      from \<open>c > 0\<close> have th': "c\<noteq>0" by auto
   7.124 +      from \<open>c > 0\<close> have cp: "c \<ge> 0" by simp
   7.125        from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   7.126        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   7.127      }
   7.128 @@ -4103,10 +4103,10 @@
   7.129      { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
   7.130        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   7.131        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   7.132 -      from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   7.133 +      from \<open>c > 0\<close> have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   7.134          by (simp add: numgcd_def)
   7.135 -      from `c > 0` have th': "c\<noteq>0" by auto
   7.136 -      from `c > 0` have cp: "c \<ge> 0" by simp
   7.137 +      from \<open>c > 0\<close> have th': "c\<noteq>0" by auto
   7.138 +      from \<open>c > 0\<close> have cp: "c \<ge> 0" by simp
   7.139        from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   7.140        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   7.141      }
   7.142 @@ -4769,7 +4769,7 @@
   7.143    ultimately show "?E" by blast
   7.144  qed
   7.145  
   7.146 -text{* The overall Part *}
   7.147 +text\<open>The overall Part\<close>
   7.148  
   7.149  lemma real_ex_int_real01:
   7.150    shows "(\<exists> (x::real). P x) = (\<exists> (i::int) (u::real). 0\<le> u \<and> u< 1 \<and> P (real i + u))"
   7.151 @@ -5518,21 +5518,21 @@
   7.152  definition
   7.153    "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))"
   7.154  
   7.155 -ML_val {* @{code mircfrqe} @{code problem1} *}
   7.156 -ML_val {* @{code mirlfrqe} @{code problem1} *}
   7.157 -ML_val {* @{code mircfrqe} @{code problem2} *}
   7.158 -ML_val {* @{code mirlfrqe} @{code problem2} *}
   7.159 -ML_val {* @{code mircfrqe} @{code problem3} *}
   7.160 -ML_val {* @{code mirlfrqe} @{code problem3} *}
   7.161 -ML_val {* @{code mircfrqe} @{code problem4} *}
   7.162 -ML_val {* @{code mirlfrqe} @{code problem4} *}
   7.163 +ML_val \<open>@{code mircfrqe} @{code problem1}\<close>
   7.164 +ML_val \<open>@{code mirlfrqe} @{code problem1}\<close>
   7.165 +ML_val \<open>@{code mircfrqe} @{code problem2}\<close>
   7.166 +ML_val \<open>@{code mirlfrqe} @{code problem2}\<close>
   7.167 +ML_val \<open>@{code mircfrqe} @{code problem3}\<close>
   7.168 +ML_val \<open>@{code mirlfrqe} @{code problem3}\<close>
   7.169 +ML_val \<open>@{code mircfrqe} @{code problem4}\<close>
   7.170 +ML_val \<open>@{code mirlfrqe} @{code problem4}\<close>
   7.171  
   7.172  
   7.173  (*code_reflect Mir
   7.174    functions mircfrqe mirlfrqe
   7.175    file "mir.ML"*)
   7.176  
   7.177 -oracle mirfr_oracle = {*
   7.178 +oracle mirfr_oracle = \<open>
   7.179  let
   7.180  
   7.181  val mk_C = @{code C} o @{code int_of_integer};
   7.182 @@ -5657,14 +5657,14 @@
   7.183      val t' = term_of_fm vs (qe (fm_of_term vs t));
   7.184    in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
   7.185  end;
   7.186 -*}
   7.187 +\<close>
   7.188  
   7.189  ML_file "mir_tac.ML"
   7.190  
   7.191 -method_setup mir = {*
   7.192 +method_setup mir = \<open>
   7.193    Scan.lift (Args.mode "no_quantify") >>
   7.194      (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
   7.195 -*} "decision procedure for MIR arithmetic"
   7.196 +\<close> "decision procedure for MIR arithmetic"
   7.197  
   7.198  
   7.199  lemma "\<forall>x::real. (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
     8.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Jun 20 16:23:56 2015 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Jun 20 16:31:44 2015 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4      Author:     Amine Chaieb
     8.5  *)
     8.6  
     8.7 -section{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
     8.8 +section\<open>A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008\<close>
     8.9  
    8.10  theory Parametric_Ferrante_Rackoff
    8.11  imports
    8.12 @@ -13,7 +13,7 @@
    8.13    "~~/src/HOL/Library/Old_Recdef"
    8.14  begin
    8.15  
    8.16 -subsection {* Terms *}
    8.17 +subsection \<open>Terms\<close>
    8.18  
    8.19  datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    8.20    | Neg tm | Sub tm tm | CNP nat poly tm
    8.21 @@ -491,7 +491,7 @@
    8.22      (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
    8.23  
    8.24  
    8.25 -subsection{* Formulae *}
    8.26 +subsection\<open>Formulae\<close>
    8.27  
    8.28  datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
    8.29    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    8.30 @@ -1623,7 +1623,7 @@
    8.31    by (induct p rule: qelim.induct) auto
    8.32  
    8.33  
    8.34 -subsection {* Core Procedure *}
    8.35 +subsection \<open>Core Procedure\<close>
    8.36  
    8.37  fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
    8.38  where
    8.39 @@ -2646,7 +2646,7 @@
    8.40  qed
    8.41  
    8.42  
    8.43 -section {* First implementation : Naive by encoding all case splits locally *}
    8.44 +section \<open>First implementation : Naive by encoding all case splits locally\<close>
    8.45  
    8.46  definition "msubsteq c t d s a r =
    8.47    evaldjf (split conj)
    8.48 @@ -3481,7 +3481,7 @@
    8.49  qed
    8.50  
    8.51  
    8.52 -section {* Second implemenation: Case splits not local *}
    8.53 +section \<open>Second implemenation: Case splits not local\<close>
    8.54  
    8.55  lemma fr_eq2:
    8.56    assumes lp: "islin p"
    8.57 @@ -4000,7 +4000,7 @@
    8.58      unfolding frpar2_def by (auto simp add: prep)
    8.59  qed
    8.60  
    8.61 -oracle frpar_oracle = {*
    8.62 +oracle frpar_oracle = \<open>
    8.63  let
    8.64  
    8.65  fun binopT T = T --> T --> T;
    8.66 @@ -4159,9 +4159,9 @@
    8.67        (frpar_procedure alternative ty ps (Thm.term_of ct))
    8.68  
    8.69  end
    8.70 -*}
    8.71 -
    8.72 -ML {*
    8.73 +\<close>
    8.74 +
    8.75 +ML \<open>
    8.76  structure Parametric_Ferrante_Rackoff =
    8.77  struct
    8.78  
    8.79 @@ -4186,15 +4186,15 @@
    8.80    end;
    8.81  
    8.82  end;
    8.83 -*}
    8.84 -
    8.85 -method_setup frpar = {*
    8.86 +\<close>
    8.87 +
    8.88 +method_setup frpar = \<open>
    8.89    Parametric_Ferrante_Rackoff.method false
    8.90 -*} "parametric QE for linear Arithmetic over fields"
    8.91 -
    8.92 -method_setup frpar2 = {*
    8.93 +\<close> "parametric QE for linear Arithmetic over fields"
    8.94 +
    8.95 +method_setup frpar2 = \<open>
    8.96    Parametric_Ferrante_Rackoff.method true
    8.97 -*} "parametric QE for linear Arithmetic over fields, Version 2"
    8.98 +\<close> "parametric QE for linear Arithmetic over fields, Version 2"
    8.99  
   8.100  lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
   8.101    apply (frpar type: 'a pars: y)
   8.102 @@ -4212,7 +4212,7 @@
   8.103    apply simp
   8.104    done
   8.105  
   8.106 -text{* Collins/Jones Problem *}
   8.107 +text\<open>Collins/Jones Problem\<close>
   8.108  (*
   8.109  lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   8.110  proof-
   8.111 @@ -4230,7 +4230,7 @@
   8.112  oops
   8.113  *)
   8.114  
   8.115 -text{* Collins/Jones Problem *}
   8.116 +text\<open>Collins/Jones Problem\<close>
   8.117  
   8.118  (*
   8.119  lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
     9.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jun 20 16:23:56 2015 +0200
     9.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jun 20 16:31:44 2015 +0200
     9.3 @@ -2,13 +2,13 @@
     9.4      Author:     Amine Chaieb
     9.5  *)
     9.6  
     9.7 -section {* Univariate Polynomials as lists *}
     9.8 +section \<open>Univariate Polynomials as lists\<close>
     9.9  
    9.10  theory Polynomial_List
    9.11  imports Complex_Main
    9.12  begin
    9.13  
    9.14 -text{* Application of polynomial as a function. *}
    9.15 +text\<open>Application of polynomial as a function.\<close>
    9.16  
    9.17  primrec (in semiring_0) poly :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a"
    9.18  where
    9.19 @@ -16,38 +16,38 @@
    9.20  | poly_Cons: "poly (h#t) x = h + x * poly t x"
    9.21  
    9.22  
    9.23 -subsection{*Arithmetic Operations on Polynomials*}
    9.24 +subsection\<open>Arithmetic Operations on Polynomials\<close>
    9.25  
    9.26 -text{*addition*}
    9.27 +text\<open>addition\<close>
    9.28  
    9.29  primrec (in semiring_0) padd :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "+++" 65)
    9.30  where
    9.31    padd_Nil:  "[] +++ l2 = l2"
    9.32  | padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t else (h + hd l2)#(t +++ tl l2))"
    9.33  
    9.34 -text{*Multiplication by a constant*}
    9.35 +text\<open>Multiplication by a constant\<close>
    9.36  primrec (in semiring_0) cmult :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "%*" 70) where
    9.37    cmult_Nil:  "c %* [] = []"
    9.38  | cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
    9.39  
    9.40 -text{*Multiplication by a polynomial*}
    9.41 +text\<open>Multiplication by a polynomial\<close>
    9.42  primrec (in semiring_0) pmult :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "***" 70)
    9.43  where
    9.44    pmult_Nil:  "[] *** l2 = []"
    9.45  | pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
    9.46                                else (h %* l2) +++ ((0) # (t *** l2)))"
    9.47  
    9.48 -text{*Repeated multiplication by a polynomial*}
    9.49 +text\<open>Repeated multiplication by a polynomial\<close>
    9.50  primrec (in semiring_0) mulexp :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a  list \<Rightarrow> 'a list" where
    9.51    mulexp_zero:  "mulexp 0 p q = q"
    9.52  | mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
    9.53  
    9.54 -text{*Exponential*}
    9.55 +text\<open>Exponential\<close>
    9.56  primrec (in semiring_1) pexp :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list"  (infixl "%^" 80) where
    9.57    pexp_0:   "p %^ 0 = [1]"
    9.58  | pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
    9.59  
    9.60 -text{*Quotient related value of dividing a polynomial by x + a*}
    9.61 +text\<open>Quotient related value of dividing a polynomial by x + a\<close>
    9.62  (* Useful for divisor properties in inductive proofs *)
    9.63  primrec (in field) "pquot" :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
    9.64  where
    9.65 @@ -55,7 +55,7 @@
    9.66  | pquot_Cons: "pquot (h#t) a =
    9.67      (if t = [] then [h] else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
    9.68  
    9.69 -text{*normalization of polynomials (remove extra 0 coeff)*}
    9.70 +text\<open>normalization of polynomials (remove extra 0 coeff)\<close>
    9.71  primrec (in semiring_0) pnormalize :: "'a list \<Rightarrow> 'a list" where
    9.72    pnormalize_Nil:  "pnormalize [] = []"
    9.73  | pnormalize_Cons: "pnormalize (h#p) =
    9.74 @@ -63,7 +63,7 @@
    9.75  
    9.76  definition (in semiring_0) "pnormal p = ((pnormalize p = p) \<and> p \<noteq> [])"
    9.77  definition (in semiring_0) "nonconstant p = (pnormal p \<and> (\<forall>x. p \<noteq> [x]))"
    9.78 -text{*Other definitions*}
    9.79 +text\<open>Other definitions\<close>
    9.80  
    9.81  definition (in ring_1) poly_minus :: "'a list \<Rightarrow> 'a list" ("-- _" [80] 80)
    9.82    where "-- p = (- 1) %* p"
    9.83 @@ -80,15 +80,15 @@
    9.84    obtains q where "poly p2 = poly (p1 *** q)"
    9.85    using assms by (auto simp add: divides_def)
    9.86  
    9.87 -    --{*order of a polynomial*}
    9.88 +    --\<open>order of a polynomial\<close>
    9.89  definition (in ring_1) order :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
    9.90    "order a p = (SOME n. ([-a, 1] %^ n) divides p \<and> ~ (([-a, 1] %^ (Suc n)) divides p))"
    9.91  
    9.92 -     --{*degree of a polynomial*}
    9.93 +     --\<open>degree of a polynomial\<close>
    9.94  definition (in semiring_0) degree :: "'a list \<Rightarrow> nat"
    9.95    where "degree p = length (pnormalize p) - 1"
    9.96  
    9.97 -     --{*squarefree polynomials --- NB with respect to real roots only.*}
    9.98 +     --\<open>squarefree polynomials --- NB with respect to real roots only.\<close>
    9.99  definition (in ring_1) rsquarefree :: "'a list \<Rightarrow> bool"
   9.100    where "rsquarefree p \<longleftrightarrow> poly p \<noteq> poly [] \<and> (\<forall>a. order a p = 0 \<or> order a p = 1)"
   9.101  
   9.102 @@ -113,7 +113,7 @@
   9.103  lemma (in semiring_0) poly_simple_add_Cons[simp]: "[a] +++ ((0)#t) = (a#t)"
   9.104    by simp
   9.105  
   9.106 -text{*Handy general properties*}
   9.107 +text\<open>Handy general properties\<close>
   9.108  
   9.109  lemma (in comm_semiring_0) padd_commut: "b +++ a = a +++ b"
   9.110  proof (induct b arbitrary: a)
   9.111 @@ -143,7 +143,7 @@
   9.112    apply (case_tac t, auto)
   9.113    done
   9.114  
   9.115 -text{*properties of evaluation of polynomials.*}
   9.116 +text\<open>properties of evaluation of polynomials.\<close>
   9.117  
   9.118  lemma (in semiring_0) poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x"
   9.119  proof(induct p1 arbitrary: p2)
   9.120 @@ -186,7 +186,7 @@
   9.121  lemma (in comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
   9.122    by (induct n) (auto simp add: poly_cmult poly_mult)
   9.123  
   9.124 -text{*More Polynomial Evaluation Lemmas*}
   9.125 +text\<open>More Polynomial Evaluation Lemmas\<close>
   9.126  
   9.127  lemma (in semiring_0) poly_add_rzero[simp]: "poly (a +++ []) x = poly a x"
   9.128    by simp
   9.129 @@ -200,8 +200,8 @@
   9.130  lemma (in comm_semiring_1) poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
   9.131    by (induct n) (auto simp add: poly_mult mult.assoc)
   9.132  
   9.133 -subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides
   9.134 - @{term "p(x)"} *}
   9.135 +subsection\<open>Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides
   9.136 + @{term "p(x)"}\<close>
   9.137  
   9.138  lemma (in comm_ring_1) lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
   9.139  proof(induct t)
   9.140 @@ -261,7 +261,7 @@
   9.141  lemma (in ring_1) poly_length_mult[simp]: "length([-a,1] *** q) = Suc (length q)"
   9.142    by auto
   9.143  
   9.144 -subsection{*Polynomial length*}
   9.145 +subsection\<open>Polynomial length\<close>
   9.146  
   9.147  lemma (in semiring_0) poly_cmult_length[simp]: "length (a %* p) = length p"
   9.148    by (induct p) auto
   9.149 @@ -279,12 +279,12 @@
   9.150  lemma (in idom) poly_mult_eq_zero_disj: "poly (p *** q) x = 0 \<longleftrightarrow> poly p x = 0 \<or> poly q x = 0"
   9.151    by (auto simp add: poly_mult)
   9.152  
   9.153 -text{*Normalisation Properties*}
   9.154 +text\<open>Normalisation Properties\<close>
   9.155  
   9.156  lemma (in semiring_0) poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
   9.157    by (induct p) auto
   9.158  
   9.159 -text{*A nontrivial polynomial of degree n has no more than n roots*}
   9.160 +text\<open>A nontrivial polynomial of degree n has no more than n roots\<close>
   9.161  lemma (in idom) poly_roots_index_lemma:
   9.162     assumes p: "poly p x \<noteq> poly [] x" and n: "length p = n"
   9.163    shows "\<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)"
   9.164 @@ -389,7 +389,7 @@
   9.165    show "poly p \<noteq> poly []" using F UNIV_ring_char_0_infinte by auto
   9.166  qed
   9.167  
   9.168 -text{*Entirety and Cancellation for polynomials*}
   9.169 +text\<open>Entirety and Cancellation for polynomials\<close>
   9.170  
   9.171  lemma (in idom_char_0) poly_entire_lemma2:
   9.172    assumes p0: "poly p \<noteq> poly []"
   9.173 @@ -451,7 +451,7 @@
   9.174  lemma (in idom) poly_exp_prime_eq_zero: "poly ([a, 1] %^ n) \<noteq> poly []"
   9.175    by auto
   9.176  
   9.177 -text{*A more constructive notion of polynomials being trivial*}
   9.178 +text\<open>A more constructive notion of polynomials being trivial\<close>
   9.179  
   9.180  lemma (in idom_char_0) poly_zero_lemma': "poly (h # t) = poly [] \<Longrightarrow> h = 0 \<and> poly t = poly []"
   9.181    apply (simp add: fun_eq)
   9.182 @@ -482,7 +482,7 @@
   9.183  
   9.184  
   9.185  
   9.186 -text{*Basics of divisibility.*}
   9.187 +text\<open>Basics of divisibility.\<close>
   9.188  
   9.189  lemma (in idom) poly_primes:
   9.190    "[a, 1] divides (p *** q) \<longleftrightarrow> [a, 1] divides p \<or> [a, 1] divides q"
   9.191 @@ -565,7 +565,7 @@
   9.192    apply (auto simp add: fun_eq)
   9.193    done
   9.194  
   9.195 -text{*At last, we can consider the order of a root.*}
   9.196 +text\<open>At last, we can consider the order of a root.\<close>
   9.197  
   9.198  lemma (in idom_char_0) poly_order_exists_lemma:
   9.199    assumes lp: "length p = d"
   9.200 @@ -650,7 +650,7 @@
   9.201          assume "\<not> poly (mulexp 0 [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc 0 *** m)"
   9.202          then have "poly q a = 0"
   9.203            by (simp add: poly_add poly_cmult)
   9.204 -        with `poly q a \<noteq> 0` show False by simp
   9.205 +        with \<open>poly q a \<noteq> 0\<close> show False by simp
   9.206        qed
   9.207      next
   9.208        case (Suc n) show ?case
   9.209 @@ -674,7 +674,7 @@
   9.210                simp del: pmult_Cons pexp_Suc)
   9.211    done
   9.212  
   9.213 -text{*Order*}
   9.214 +text\<open>Order\<close>
   9.215  
   9.216  lemma some1_equalityD: "n = (SOME n. P n) \<Longrightarrow> \<exists>!n. P n \<Longrightarrow> P n"
   9.217    by (blast intro: someI2)
   9.218 @@ -745,7 +745,7 @@
   9.219    apply (auto simp add: poly_mult fun_eq poly_exp ac_simps simp del: pmult_Cons)
   9.220    done
   9.221  
   9.222 -text{*Important composition properties of orders.*}
   9.223 +text\<open>Important composition properties of orders.\<close>
   9.224  lemma order_mult:
   9.225    "poly (p *** q) \<noteq> poly [] \<Longrightarrow>
   9.226      order a (p *** q) = order a p + order (a::'a::{idom_char_0}) q"
   9.227 @@ -822,12 +822,12 @@
   9.228    done
   9.229  
   9.230  
   9.231 -text{*Normalization of a polynomial.*}
   9.232 +text\<open>Normalization of a polynomial.\<close>
   9.233  
   9.234  lemma (in semiring_0) poly_normalize[simp]: "poly (pnormalize p) = poly p"
   9.235    by (induct p) (auto simp add: fun_eq)
   9.236  
   9.237 -text{*The degree of a polynomial.*}
   9.238 +text\<open>The degree of a polynomial.\<close>
   9.239  
   9.240  lemma (in semiring_0) lemma_degree_zero: "list_all (%c. c = 0) p \<longleftrightarrow> pnormalize p = []"
   9.241    by (induct p) auto
   9.242 @@ -1032,13 +1032,13 @@
   9.243      by auto
   9.244  qed
   9.245  
   9.246 -text{*Tidier versions of finiteness of roots.*}
   9.247 +text\<open>Tidier versions of finiteness of roots.\<close>
   9.248  
   9.249  lemma (in idom_char_0) poly_roots_finite_set:
   9.250    "poly p \<noteq> poly [] \<Longrightarrow> finite {x. poly p x = 0}"
   9.251    unfolding poly_roots_finite .
   9.252  
   9.253 -text{*bound for polynomial.*}
   9.254 +text\<open>bound for polynomial.\<close>
   9.255  
   9.256  lemma poly_mono: "abs(x) \<le> k \<Longrightarrow> abs(poly p (x::'a::{linordered_idom})) \<le> poly (map abs p) k"
   9.257    apply (induct p)
    10.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Jun 20 16:23:56 2015 +0200
    10.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Jun 20 16:31:44 2015 +0200
    10.3 @@ -2,7 +2,7 @@
    10.4      Author:     Amine Chaieb
    10.5  *)
    10.6  
    10.7 -section {* Rational numbers as pairs *}
    10.8 +section \<open>Rational numbers as pairs\<close>
    10.9  
   10.10  theory Rat_Pair
   10.11  imports Complex_Main
   10.12 @@ -66,7 +66,7 @@
   10.13    ultimately show ?thesis by blast
   10.14  qed
   10.15  
   10.16 -text {* Arithmetic over Num *}
   10.17 +text \<open>Arithmetic over Num\<close>
   10.18  
   10.19  definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "+\<^sub>N" 60) where
   10.20    "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
   10.21 @@ -129,7 +129,7 @@
   10.22    by (simp_all add: isnormNum_def)
   10.23  
   10.24  
   10.25 -text {* Relations over Num *}
   10.26 +text \<open>Relations over Num\<close>
   10.27  
   10.28  definition Nlt0:: "Num \<Rightarrow> bool"  ("0>\<^sub>N")
   10.29    where "Nlt0 = (\<lambda>(a,b). a < 0)"
   10.30 @@ -206,7 +206,7 @@
   10.31      by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
   10.32    then have "of_int x / of_int d = ?t / of_int d"
   10.33      using cong[OF refl[of ?f] eq] by simp
   10.34 -  then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
   10.35 +  then show ?thesis by (simp add: add_divide_distrib algebra_simps \<open>d ~= 0\<close>)
   10.36  qed
   10.37  
   10.38  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
    11.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 16:23:56 2015 +0200
    11.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 16:31:44 2015 +0200
    11.3 @@ -2,13 +2,13 @@
    11.4      Author:     Amine Chaieb
    11.5  *)
    11.6  
    11.7 -section {* Implementation and verification of multivariate polynomials *}
    11.8 +section \<open>Implementation and verification of multivariate polynomials\<close>
    11.9  
   11.10  theory Reflected_Multivariate_Polynomial
   11.11  imports Complex_Main Rat_Pair Polynomial_List
   11.12  begin
   11.13  
   11.14 -subsection{* Datatype of polynomial expressions *}
   11.15 +subsection\<open>Datatype of polynomial expressions\<close>
   11.16  
   11.17  datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
   11.18    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
   11.19 @@ -17,7 +17,7 @@
   11.20  abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
   11.21  
   11.22  
   11.23 -subsection{* Boundedness, substitution and all that *}
   11.24 +subsection\<open>Boundedness, substitution and all that\<close>
   11.25  
   11.26  primrec polysize:: "poly \<Rightarrow> nat"
   11.27  where
   11.28 @@ -30,7 +30,7 @@
   11.29  | "polysize (Pw p n) = 1 + polysize p"
   11.30  | "polysize (CN c n p) = 4 + polysize c + polysize p"
   11.31  
   11.32 -primrec polybound0:: "poly \<Rightarrow> bool" -- {* a poly is INDEPENDENT of Bound 0 *}
   11.33 +primrec polybound0:: "poly \<Rightarrow> bool" -- \<open>a poly is INDEPENDENT of Bound 0\<close>
   11.34  where
   11.35    "polybound0 (C c) \<longleftrightarrow> True"
   11.36  | "polybound0 (Bound n) \<longleftrightarrow> n > 0"
   11.37 @@ -41,7 +41,7 @@
   11.38  | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
   11.39  | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
   11.40  
   11.41 -primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- {* substitute a poly into a poly for Bound 0 *}
   11.42 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- \<open>substitute a poly into a poly for Bound 0\<close>
   11.43  where
   11.44    "polysubst0 t (C c) = C c"
   11.45  | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
   11.46 @@ -66,7 +66,7 @@
   11.47  | "decrpoly a = a"
   11.48  
   11.49  
   11.50 -subsection{* Degrees and heads and coefficients *}
   11.51 +subsection\<open>Degrees and heads and coefficients\<close>
   11.52  
   11.53  fun degree :: "poly \<Rightarrow> nat"
   11.54  where
   11.55 @@ -110,7 +110,7 @@
   11.56  | "headconst (C n) = n"
   11.57  
   11.58  
   11.59 -subsection{* Operations for normalization *}
   11.60 +subsection\<open>Operations for normalization\<close>
   11.61  
   11.62  declare if_cong[fundef_cong del]
   11.63  declare let_cong[fundef_cong del]
   11.64 @@ -195,7 +195,7 @@
   11.65       in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))"
   11.66  
   11.67  
   11.68 -subsection {* Pseudo-division *}
   11.69 +subsection \<open>Pseudo-division\<close>
   11.70  
   11.71  definition shift1 :: "poly \<Rightarrow> poly"
   11.72    where "shift1 p = CN 0\<^sub>p 0 p"
   11.73 @@ -233,7 +233,7 @@
   11.74  | "poly_deriv p = 0\<^sub>p"
   11.75  
   11.76  
   11.77 -subsection{* Semantics of the polynomial representation *}
   11.78 +subsection\<open>Semantics of the polynomial representation\<close>
   11.79  
   11.80  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
   11.81  where
   11.82 @@ -259,7 +259,7 @@
   11.83  lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
   11.84  
   11.85  
   11.86 -subsection {* Normal form and normalization *}
   11.87 +subsection \<open>Normal form and normalization\<close>
   11.88  
   11.89  fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   11.90  where
   11.91 @@ -273,7 +273,7 @@
   11.92  definition isnpoly :: "poly \<Rightarrow> bool"
   11.93    where "isnpoly p = isnpolyh p 0"
   11.94  
   11.95 -text{* polyadd preserves normal forms *}
   11.96 +text\<open>polyadd preserves normal forms\<close>
   11.97  
   11.98  lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
   11.99  proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
  11.100 @@ -380,7 +380,7 @@
  11.101  lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
  11.102    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
  11.103  
  11.104 -text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
  11.105 +text\<open>The degree of addition and other general lemmas needed for the normal form of polymul\<close>
  11.106  
  11.107  lemma polyadd_different_degreen:
  11.108    assumes "isnpolyh p n0"
  11.109 @@ -720,7 +720,7 @@
  11.110  qed
  11.111  
  11.112  
  11.113 -text{* polyneg is a negation and preserves normal forms *}
  11.114 +text\<open>polyneg is a negation and preserves normal forms\<close>
  11.115  
  11.116  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
  11.117    by (induct p rule: polyneg.induct) auto
  11.118 @@ -738,7 +738,7 @@
  11.119    using isnpoly_def polyneg_normh by simp
  11.120  
  11.121  
  11.122 -text{* polysub is a substraction and preserves normal forms *}
  11.123 +text\<open>polysub is a substraction and preserves normal forms\<close>
  11.124  
  11.125  lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
  11.126    by (simp add: polysub_def)
  11.127 @@ -762,7 +762,7 @@
  11.128    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
  11.129      (auto simp: Nsub0[simplified Nsub_def] Let_def)
  11.130  
  11.131 -text{* polypow is a power function and preserves normal forms *}
  11.132 +text\<open>polypow is a power function and preserves normal forms\<close>
  11.133  
  11.134  lemma polypow[simp]:
  11.135    "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
  11.136 @@ -830,7 +830,7 @@
  11.137    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
  11.138    by (simp add: polypow_normh isnpoly_def)
  11.139  
  11.140 -text{* Finally the whole normalization *}
  11.141 +text\<open>Finally the whole normalization\<close>
  11.142  
  11.143  lemma polynate [simp]:
  11.144    "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
  11.145 @@ -843,7 +843,7 @@
  11.146       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
  11.147        simp_all add: isnpoly_def)
  11.148  
  11.149 -text{* shift1 *}
  11.150 +text\<open>shift1\<close>
  11.151  
  11.152  
  11.153  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
  11.154 @@ -905,7 +905,7 @@
  11.155    using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
  11.156  
  11.157  
  11.158 -subsection {* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
  11.159 +subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
  11.160  
  11.161  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
  11.162  proof (induct p arbitrary: n rule: poly.induct, auto)
  11.163 @@ -913,7 +913,7 @@
  11.164    then have "n = Suc (n - 1)"
  11.165      by simp
  11.166    then have "isnpolyh p (Suc (n - 1))"
  11.167 -    using `isnpolyh p n` by simp
  11.168 +    using \<open>isnpolyh p n\<close> by simp
  11.169    with goal1(2) show ?case
  11.170      by simp
  11.171  qed
  11.172 @@ -1078,7 +1078,7 @@
  11.173    using wf_bs_polyadd wf_bs_polyneg by blast
  11.174  
  11.175  
  11.176 -subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *}
  11.177 +subsection \<open>Canonicity of polynomial representation, see lemma isnpolyh_unique\<close>
  11.178  
  11.179  definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
  11.180  definition "polypoly' bs p = map (Ipoly bs \<circ> decrpoly) (coefficients p)"
  11.181 @@ -1165,7 +1165,7 @@
  11.182    using nq eq
  11.183  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
  11.184    case less
  11.185 -  note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
  11.186 +  note np = \<open>isnpolyh p n0\<close> and zp = \<open>\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)\<close>
  11.187    {
  11.188      assume nz: "maxindex p = 0"
  11.189      then obtain c where "p = C c"
  11.190 @@ -1254,7 +1254,7 @@
  11.191  qed
  11.192  
  11.193  
  11.194 -text{* consequences of unicity on the algorithms for polynomial normalization *}
  11.195 +text\<open>consequences of unicity on the algorithms for polynomial normalization\<close>
  11.196  
  11.197  lemma polyadd_commute:
  11.198    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
  11.199 @@ -1328,7 +1328,7 @@
  11.200    unfolding poly_nate_polypoly' by auto
  11.201  
  11.202  
  11.203 -subsection{* heads, degrees and all that *}
  11.204 +subsection\<open>heads, degrees and all that\<close>
  11.205  
  11.206  lemma degree_eq_degreen0: "degree p = degreen p 0"
  11.207    by (induct p rule: degree.induct) simp_all
  11.208 @@ -1647,7 +1647,7 @@
  11.209    by (induct p arbitrary: n rule: degree.induct) auto
  11.210  
  11.211  
  11.212 -subsection {* Correctness of polynomial pseudo division *}
  11.213 +subsection \<open>Correctness of polynomial pseudo division\<close>
  11.214  
  11.215  lemma polydivide_aux_properties:
  11.216    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
  11.217 @@ -1668,7 +1668,7 @@
  11.218    let ?p' = "funpow (degree s - n) shift1 p"
  11.219    let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p"
  11.220    let ?akk' = "a ^\<^sub>p (k' - k)"
  11.221 -  note ns = `isnpolyh s n1`
  11.222 +  note ns = \<open>isnpolyh s n1\<close>
  11.223    from np have np0: "isnpolyh p 0"
  11.224      using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp
  11.225    have np': "isnpolyh ?p' 0"
  11.226 @@ -1973,7 +1973,7 @@
  11.227  qed
  11.228  
  11.229  
  11.230 -subsection {* More about polypoly and pnormal etc *}
  11.231 +subsection \<open>More about polypoly and pnormal etc\<close>
  11.232  
  11.233  definition "isnonconstant p \<longleftrightarrow> \<not> isconstant p"
  11.234  
  11.235 @@ -2071,7 +2071,7 @@
  11.236  qed
  11.237  
  11.238  
  11.239 -section {* Swaps ; Division by a certain variable *}
  11.240 +section \<open>Swaps ; Division by a certain variable\<close>
  11.241  
  11.242  primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
  11.243  where
    12.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sat Jun 20 16:23:56 2015 +0200
    12.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sat Jun 20 16:31:44 2015 +0200
    12.3 @@ -4,7 +4,7 @@
    12.4  imports Complex_Main "../Approximation"
    12.5  begin
    12.6  
    12.7 -text {*
    12.8 +text \<open>
    12.9  
   12.10  Here are some examples how to use the approximation method.
   12.11  
   12.12 @@ -31,7 +31,7 @@
   12.13  specify the amount of derivations to compute. When using taylor series expansion
   12.14  only one variable can be used.
   12.15  
   12.16 -*}
   12.17 +\<close>
   12.18  
   12.19  section "Compute some transcendental values"
   12.20  
    13.1 --- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Sat Jun 20 16:23:56 2015 +0200
    13.2 +++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Sat Jun 20 16:31:44 2015 +0200
    13.3 @@ -1,6 +1,6 @@
    13.4  (*  Author:     Bernhard Haeupler *)
    13.5  
    13.6 -section {* Some examples demonstrating the comm-ring method *}
    13.7 +section \<open>Some examples demonstrating the comm-ring method\<close>
    13.8  
    13.9  theory Commutative_Ring_Ex
   13.10  imports "../Commutative_Ring"
    14.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Sat Jun 20 16:23:56 2015 +0200
    14.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Sat Jun 20 16:31:44 2015 +0200
    14.3 @@ -1,6 +1,6 @@
    14.4  (* Author:     Amine Chaieb, TU Muenchen *)
    14.5  
    14.6 -section {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
    14.7 +section \<open>Examples for Ferrante and Rackoff's quantifier elimination procedure\<close>
    14.8  
    14.9  theory Dense_Linear_Order_Ex
   14.10  imports "../Dense_Linear_Order"