# HG changeset patch
# User wenzelm
# Date 1528404400 -7200
# Node ID 9a24536225965c99bd9142fe91d54fb4c4cda504
# Parent  6beb45f6cf67e3a3cdb09607c79245b2b9f4c1e3# Parent  fd61a2e4e1f9ac4601dae8c1b389ecbd07ca75ff
merged

diff -r 6beb45f6cf67 -r 9a2453622596 src/HOL/SPARK/Manual/Example_Verification.thy
--- a/src/HOL/SPARK/Manual/Example_Verification.thy	Thu Jun 07 19:36:12 2018 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Thu Jun 07 22:46:40 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