--- a/src/HOL/Number_Theory/Eratosthenes.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Sat Jan 05 17:24:33 2019 +0100
@@ -23,7 +23,7 @@
subsection \<open>Main corpus\<close>
-text \<open>The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}.\<close>
+text \<open>The sieve is modelled as a list of booleans, where \<^const>\<open>False\<close> means \emph{marked out}.\<close>
type_synonym marks = "bool list"
@@ -175,8 +175,8 @@
\begin{itemize}
- \item @{const sieve} can abort as soon as @{term n} is too big to let
- @{const mark_out} have any effect.
+ \item \<^const>\<open>sieve\<close> can abort as soon as \<^term>\<open>n\<close> is too big to let
+ \<^const>\<open>mark_out\<close> have any effect.
\item Search for further primes can be given up as soon as the search
position exceeds the square root of the maximum candidate.