48 now, but some parts, particularly the chapters on tactics, are still |
48 now, but some parts, particularly the chapters on tactics, are still |
49 useful. |
49 useful. |
50 |
50 |
51 \item[The Isar Reference Manual] provides specification material (like grammars, |
51 \item[The Isar Reference Manual] provides specification material (like grammars, |
52 examples and so on) about Isar and its implementation. It is currently in |
52 examples and so on) about Isar and its implementation. It is currently in |
53 the process of being updated. . |
53 the process of being updated. |
54 \end{description} |
54 \end{description} |
55 |
55 |
56 Then of course there is: |
56 Then of course there is: |
57 |
57 |
58 \begin{description} |
58 \begin{description} |
59 \item[The code] is of course the ultimate reference for how |
59 \item[The code] is of course the ultimate reference for how |
60 things really work. Therefore you should not hesitate to look at the |
60 things really work. Therefore you should not hesitate to look at the |
61 way things are actually implemented. More importantly, it is often |
61 way things are actually implemented. More importantly, it is often |
62 good to look at code that does similar things as you want to do and |
62 good to look at code that does similar things as you want to do and |
63 to learn from other people's code. |
63 to learn from that code. |
64 \end{description} |
64 \end{description} |
65 |
65 |
66 *} |
66 *} |
67 |
67 |
68 section {* Typographic Conventions *} |
68 section {* Typographic Conventions *} |
106 |
106 |
107 \begin{readmore} |
107 \begin{readmore} |
108 Further information or pointers to files. |
108 Further information or pointers to files. |
109 \end{readmore} |
109 \end{readmore} |
110 |
110 |
|
111 A few exercises a scattered around the text. Their solutions are given |
|
112 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
|
113 to solve the exercises on your own. |
|
114 |
111 *} |
115 *} |
112 |
116 |
113 section {* Acknowledgements *} |
117 section {* Acknowledgements *} |
114 |
118 |
115 text {* |
119 text {* |
116 Financial support for this tutorial was provided by the German |
120 Financial support for this tutorial was provided by the German |
117 Research Council (DFG) under grant number URB 165/5-1. The following |
121 Research Council (DFG) under grant number URB 165/5-1. The following |
118 people contributed: |
122 people contributed to the text: |
119 |
123 |
120 \begin{itemize} |
124 \begin{itemize} |
121 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
125 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
122 \simpleinductive-package and the code for the @{text |
126 \simpleinductive-package and the code for the @{text |
123 "chunk"}-antiquotation. He also wrote the first version of the chapter |
127 "chunk"}-antiquotation. He also wrote the first version of the chapter |