equal
deleted
inserted
replaced
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. The code provided in the Cookbook is |
11 solving common problems. The code provided in the Cookbook is |
12 checked against recent versions of Isabelle. |
12 as far as possible checked against recent versions of Isabelle. |
13 *} |
13 *} |
14 |
14 |
15 section {* Intended Audience and Prior Knowledge *} |
15 section {* Intended Audience and Prior Knowledge *} |
16 |
16 |
17 text {* |
17 text {* |
18 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 |
19 for writing theories and proofs. We also assume that readers are |
19 for writing theories and proofs. We also assume that readers are |
20 familiar with the functional programming language ML, the language in |
20 familiar with the functional programming language ML, the language in |
21 which 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 |
22 these two subjects, you should first work through the Isabelle/HOL |
22 these two subjects, you should first work through the Isabelle/HOL |
23 tutorial \cite{isa-tutorial} or Paulson's book on ML |
23 tutorial \cite{isa-tutorial} or Paulson's book on ML |