equal
deleted
inserted
replaced
37 (usually {\HOL}) already pre-loaded. |
37 (usually {\HOL}) already pre-loaded. |
38 |
38 |
39 Subsequently, we assume that the \texttt{isabelle} executable is determined |
39 Subsequently, we assume that the \texttt{isabelle} executable is determined |
40 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome |
40 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome |
41 \rangle\)/bin} to your search path.\footnote{Depending on your installation, |
41 \rangle\)/bin} to your search path.\footnote{Depending on your installation, |
42 there might be also stand-alone binaries located in some global directory |
42 there may be stand-alone binaries located in some global directory such as |
43 such as \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle |
43 \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle isabellehome |
44 isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool |
44 \rangle\)/bin/isabelle}, though! See \texttt{isatool install} in |
45 install} in \emph{The Isabelle System Manual} of how to do this properly.} |
45 \emph{The Isabelle System Manual} of how to do this properly.} |
46 |
46 |
47 \medskip |
47 \medskip |
48 |
48 |
49 The object-logic image to load may be also specified explicitly as an argument |
49 The object-logic image to load may be also specified explicitly as an argument |
50 to the {\tt isabelle} command, e.g. |
50 to the {\tt isabelle} command, e.g. |