equal
deleted
inserted
replaced
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 in 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. |
12 *} |
12 *} |
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. We also assume that readers are |
18 for writing theories and proofs. We also assume that readers are |
19 familiar with the Standard ML, the 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 either 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 |
25 *} |
25 *} |