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 Standard ML, the programming language in which |
19 familiar with Standard ML (SML), 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} or Paulson's book on Standard ML |
22 tutorial \cite{isa-tutorial} or Paulson's book on SML |
23 \cite{paulson-ml2}. |
23 \cite{paulson-ml2}. |
24 |
24 |
25 *} |
25 *} |
26 |
26 |
27 section {* Existing Documentation *} |
27 section {* Existing Documentation *} |
55 way things are actually implemented. More importantly, it is often |
55 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 |
56 good to look at code that does similar things as you want to do, to |
57 learn from other people's code. |
57 learn from other people's code. |
58 \end{description} |
58 \end{description} |
59 |
59 |
60 Since Isabelle is not a finished product, these manuals, just like |
60 The Cookbook is written in such a way that the code examples in it are |
61 the implementation itself, are always under construction. This can |
61 synchronised with fairly recent versions of the code. |
62 be difficult and frustrating at times, especially when interfaces changes |
62 |
63 occur frequently. But it is a reality that progress means changing |
|
64 things (FIXME: need some short and convincing comment that this |
|
65 is a strategy, not a problem that should be solved). |
|
66 *} |
63 *} |
67 |
64 |
68 |
65 |
69 end |
66 end |