4 begin |
4 begin |
5 |
5 |
6 chapter {* Introduction *} |
6 chapter {* Introduction *} |
7 |
7 |
8 text {* |
8 text {* |
9 The purpose of this cookbook is to guide the reader through the |
9 The purpose of this Cookbook is to guide the reader through the |
10 first steps of Isabelle programming, and to provide recipes for |
10 first steps of Isabelle programming, and to provide recipes for |
11 solving common problems. |
11 solving common problems. The code provided in the Cookbook is |
|
12 checked against recent versions of Isabelle. |
12 *} |
13 *} |
13 |
14 |
14 section {* Intended Audience and Prior Knowledge *} |
15 section {* Intended Audience and Prior Knowledge *} |
15 |
16 |
16 text {* |
17 text {* |
17 This cookbook targets an audience who already knows how to use Isabelle |
18 This cookbook targets an audience who already knows how to use Isabelle |
18 for writing theories and proofs. We also assume that readers are |
19 for writing theories and proofs. We also assume that readers are |
19 familiar with Standard ML (SML), the programming language in which |
20 familiar with the functional programming language ML, the language in |
20 most of Isabelle is implemented. If you are unfamiliar with either of |
21 which most of Isabelle is implemented. If you are unfamiliar with either of |
21 these two subjects, you should first work through the Isabelle/HOL |
22 these two subjects, you should first work through the Isabelle/HOL |
22 tutorial \cite{isa-tutorial} or Paulson's book on SML |
23 tutorial \cite{isa-tutorial} or Paulson's book on ML |
23 \cite{paulson-ml2}. |
24 \cite{paulson-ml2}. |
24 |
25 |
25 *} |
26 *} |
26 |
27 |
27 section {* Existing Documentation *} |
28 section {* Existing Documentation *} |
55 way things are actually implemented. More importantly, it is often |
56 way things are actually implemented. More importantly, it is often |
56 good to look at code that does similar things as you want to do, to |
57 good to look at code that does similar things as you want to do, to |
57 learn from other people's code. |
58 learn from other people's code. |
58 \end{description} |
59 \end{description} |
59 |
60 |
60 The Cookbook is written in such a way that the code examples in it are |
|
61 checked against recent versions of the code. |
|
62 |
|
63 *} |
61 *} |
64 |
62 |
65 |
63 |
66 end |
64 end |