--- a/src/HOL/Decision_Procs/Approximation.thy Tue Nov 10 14:18:41 2015 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Nov 10 14:43:29 2015 +0000
@@ -18,7 +18,7 @@
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" |