--- a/src/HOL/SPARK/Manual/Example_Verification.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy Thu Jun 07 16:09:43 2018 +0200
@@ -49,7 +49,7 @@
\isa{\isacommand{begin}} keyword. In order to interactively process the theory
shown in \figref{fig:gcd-proof}, we start Isabelle with the command
\begin{verbatim}
- isabelle emacs -l HOL-SPARK Greatest_Common_Divisor.thy
+ isabelle jedit -l HOL-SPARK Greatest_Common_Divisor.thy
\end{verbatim}
The option ``\texttt{-l HOL-SPARK}'' instructs Isabelle to load the right
object logic image containing the verification environment. Each proof function