merged
authorwenzelm
Thu Jun 07 22:46:40 2018 +0200 (11 months ago)
changeset 684089a2453622596
parent 68406 6beb45f6cf67
parent 68407 fd61a2e4e1f9
child 68409 c8c3136e3ba7
merged
     1.1 --- a/src/HOL/SPARK/Manual/Example_Verification.thy	Thu Jun 07 19:36:12 2018 +0200
     1.2 +++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Thu Jun 07 22:46:40 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