equal
deleted
inserted
replaced
493 A read-only @{verbatim Test} session may be started by: |
493 A read-only @{verbatim Test} session may be started by: |
494 \begin{ttbox} |
494 \begin{ttbox} |
495 isabelle-process -r Test |
495 isabelle-process -r Test |
496 \end{ttbox} |
496 \end{ttbox} |
497 |
497 |
498 \medskip Note that manual session management like this does |
|
499 \emph{not} provide proper setup for theory presentation. This would |
|
500 require @{tool usedir}. |
|
501 |
|
502 \bigskip The next example demonstrates batch execution of Isabelle. |
498 \bigskip The next example demonstrates batch execution of Isabelle. |
503 We retrieve the @{verbatim Main} theory value from the theory loader |
499 We retrieve the @{verbatim Main} theory value from the theory loader |
504 within ML (observe the delicate quoting rules for the Bash shell |
500 within ML (observe the delicate quoting rules for the Bash shell |
505 vs.\ ML): |
501 vs.\ ML): |
506 \begin{ttbox} |
502 \begin{ttbox} |