13 |
13 |
14 section {* Intended Audience and Prior Knowledge *} |
14 section {* Intended Audience and Prior Knowledge *} |
15 |
15 |
16 text {* |
16 text {* |
17 This cookbook targets an audience who already knows how to use Isabelle |
17 This cookbook targets an audience who already knows how to use Isabelle |
18 for writing theories and proofs. It is also assumed that the reader is |
18 for writing theories and proofs. We also assume that readers are |
19 familiar with the \emph{Standard ML} programming language, in which |
19 familiar with the Standard ML, the programming language in which |
20 most of Isabelle is implemented. If you are unfamiliar with any of |
20 most of Isabelle is implemented. If you are unfamiliar with any of |
21 these two subjects, you should first work through the Isabelle/HOL |
21 these two subjects, you should first work through the Isabelle/HOL |
22 tutorial \cite{isa-tutorial} and Paulson's book on Standard ML |
22 tutorial \cite{isa-tutorial} and Paulson's book on Standard ML |
23 \cite{paulson-ml2}. |
23 \cite{paulson-ml2}. |
24 |
24 |
26 |
26 |
27 section {* Existing Documentation *} |
27 section {* Existing Documentation *} |
28 |
28 |
29 text {* |
29 text {* |
30 |
30 |
31 The following documents about ML-coding for Isabelle already exist (they are |
31 The following documentation about Isabelle programming already exist (they are |
32 included in the Isabelle distribution): |
32 included in the distribution of Isabelle): |
33 |
33 |
34 \begin{description} |
34 \begin{description} |
35 \item[The Implementation Manual] describes Isabelle |
35 \item[The Implementation Manual] describes Isabelle |
36 from a programmer's perspective, documenting both the underlying |
36 from a programmer's perspective, documenting both the underlying |
37 concepts and the concrete interfaces. |
37 concepts and some of the interfaces. |
38 |
38 |
39 \item[The Isabelle Reference Manual] is an older document that used |
39 \item[The Isabelle Reference Manual] is an older document that used |
40 to be the main reference, when all reasoning happened on the ML |
40 to be the main reference at a time when all proof scripts were written |
41 level. Many parts of it are outdated now, but some parts, mainly the |
41 on the ML level. Many parts of this manual are outdated now, but some |
42 chapters on tactics, are still useful. |
42 parts, mainly the chapters on tactics, are still useful. |
43 \end{description} |
43 \end{description} |
44 |
44 |
45 Then of ourse there is: |
45 Then of ourse there is: |
46 |
46 |
47 \begin{description} |
47 \begin{description} |