# HG changeset patch
# User wenzelm
# Date 1528380583 -7200
# Node ID fd61a2e4e1f9ac4601dae8c1b389ecbd07ca75ff
# Parent  6a0852b8e5a8cff58a00a9e6e24724051c7d051b
isabelle emacs no longer exists;

diff -r 6a0852b8e5a8 -r fd61a2e4e1f9 src/HOL/SPARK/Manual/Example_Verification.thy
--- 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