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