equal
deleted
inserted
replaced
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 Standard ML, the programming language in which |
20 most of Isabelle is implemented. If you are unfamiliar with either 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} or Paulson's book on Standard ML |
23 \cite{paulson-ml2}. |
23 \cite{paulson-ml2}. |
24 |
24 |
25 *} |
25 *} |
26 |
26 |
27 section {* Existing Documentation *} |
27 section {* Existing Documentation *} |