src/HOL/Decision_Procs/Approximation.thy

 declare powr_neg_one [simp]
 declare powr_neg_numeral [simp]
 
 section "Horner Scheme"
 
-subsection \<open>Define auxiliary helper @{text horner} function\<close>
+subsection \<open>Define auxiliary helper \<open>horner\<close> function\<close>
 
 primrec horner :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> real" where
 "horner F G 0 i k x       = 0" |
 "horner F G (Suc n) i k x = 1 / k - x * horner F G n (F i) (G i k) x"