equal
deleted
inserted
replaced
14 *} |
14 *} |
15 |
15 |
16 section {* Intended Audience and Prior Knowledge *} |
16 section {* Intended Audience and Prior Knowledge *} |
17 |
17 |
18 text {* |
18 text {* |
19 This Cookbook targets an audience who already knows how to use Isabelle |
19 This Cookbook targets readers who already know how to use Isabelle |
20 for writing theories and proofs. We also assume that readers are |
20 for writing theories and proofs. We also assume that readers are |
21 familiar with the functional programming language ML, the language in |
21 familiar with the functional programming language ML, the language in |
22 which most of Isabelle is implemented. If you are unfamiliar with either of |
22 which most of Isabelle is implemented. If you are unfamiliar with either of |
23 these two subjects, you should first work through the Isabelle/HOL |
23 these two subjects, you should first work through the Isabelle/HOL |
24 tutorial \cite{isa-tutorial} or Paulson's book on ML |
24 tutorial \cite{isa-tutorial} or Paulson's book on ML |