31 The following documentation about Isabelle programming already exists (and is |
31 The following documentation about Isabelle programming already exists (and is |
32 part of the distribution of Isabelle): |
32 part of the distribution of Isabelle): |
33 |
33 |
34 \begin{description} |
34 \begin{description} |
35 \item[The Implementation Manual] describes Isabelle |
35 \item[The Implementation Manual] describes Isabelle |
36 from a programmer's perspective, documenting both the underlying |
36 from a high-level perspective, documenting both the underlying |
37 concepts and some of the interfaces. |
37 concepts and some of the interfaces. |
38 |
38 |
39 \item[The Isabelle Reference Manual] is an older document that used |
39 \item[The Isabelle Reference Manual] is an older document that used |
40 to be the main reference at a time when all proof scripts were written |
40 to be the main reference of Isabelle at a time when all proof scripts |
41 on the ML level. Many parts of this manual are outdated now, but some |
41 were written on the ML level. Many parts of this manual are outdated |
42 parts, particularly the chapters on tactics, are still useful. |
42 now, but some parts, particularly the chapters on tactics, are still |
|
43 useful. |
|
44 |
|
45 \item[The Isar Reference Manual] is also an older document that provides |
|
46 material about Isar and its implementation. Some material in it |
|
47 is still useful. |
43 \end{description} |
48 \end{description} |
44 |
49 |
45 Then of course there is: |
50 Then of course there is: |
46 |
51 |
47 \begin{description} |
52 \begin{description} |