equal
deleted
inserted
replaced
7 text {* |
7 text {* |
8 |
8 |
9 \begin{itemize} |
9 \begin{itemize} |
10 \item The Cookbook can be compiled on the command-line with: |
10 \item The Cookbook can be compiled on the command-line with: |
11 |
11 |
12 \begin{center} |
12 @{text [display] "$ isabelle make"} |
13 @{text "isabelle make"} |
|
14 \end{center} |
|
15 |
13 |
16 You very likely need a recent snapshot of Isabelle in order to compile |
14 You very likely need a recent snapshot of Isabelle in order to compile |
17 the Cookbook. Some parts of the Cookbook also rely on compilation with |
15 the Cookbook. Some parts of the Cookbook also rely on compilation with |
18 PolyML. |
16 PolyML. |
19 |
17 |