12 Isabelle programming, and also explain tricks of the trade. The best way to |
12 Isabelle programming, and also explain tricks of the trade. The best way to |
13 get to know the ML-level of Isabelle is by experimenting with the many code |
13 get to know the ML-level of Isabelle is by experimenting with the many code |
14 examples included in the tutorial. The code is as far as possible checked |
14 examples included in the tutorial. The code is as far as possible checked |
15 against recent versions of Isabelle. If something does not work, then |
15 against recent versions of Isabelle. If something does not work, then |
16 please let us know. If you have comments, criticism or like to add to the |
16 please let us know. If you have comments, criticism or like to add to the |
17 tutorial, feel free---you are most welcome! The tutorial is meant to be |
17 tutorial, please feel free---you are most welcome! The tutorial is meant to be |
18 gentle and comprehensive. To achieve this we need your feedback. |
18 gentle and comprehensive. To achieve this we need your feedback. |
19 *} |
19 *} |
20 |
20 |
21 section {* Intended Audience and Prior Knowledge *} |
21 section {* Intended Audience and Prior Knowledge *} |
22 |
22 |
36 |
36 |
37 The following documentation about Isabelle programming already exists (and is |
37 The following documentation about Isabelle programming already exists (and is |
38 part of the distribution of Isabelle): |
38 part of the distribution of Isabelle): |
39 |
39 |
40 \begin{description} |
40 \begin{description} |
41 \item[The Implementation Manual] describes Isabelle |
41 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
42 from a high-level perspective, documenting both the underlying |
42 from a high-level perspective, documenting both the underlying |
43 concepts and some of the interfaces. |
43 concepts and some of the interfaces. |
44 |
44 |
45 \item[The Isabelle Reference Manual] is an older document that used |
45 \item[The Isabelle Reference Manual] is an older document that used |
46 to be the main reference of Isabelle at a time when all proof scripts |
46 to be the main reference of Isabelle at a time when all proof scripts |
47 were written on the ML-level. Many parts of this manual are outdated |
47 were written on the ML-level. Many parts of this manual are outdated |
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] is also an older document that provides |
51 \item[The Isar Reference Manual] provides specification material (like grammars, |
52 material about Isar and its implementation. Some material in it |
52 examples and so on) about Isar and its implementation. It is currently in |
53 is still useful. |
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, and then look at the solutions. |
|
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 |
124 describing the package and has been helpful \emph{beyond measure} with |
128 describing the package and has been helpful \emph{beyond measure} with |
125 answering questions about Isabelle. |
129 answering questions about Isabelle. |
126 |
130 |
127 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
131 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
128 \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. |
132 \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. |
129 He also wrote section \ref{sec:conversion}. |
133 He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}. |
130 |
134 |
131 \item {\bf Jeremy Dawson} wrote the first version of the chapter |
135 \item {\bf Jeremy Dawson} wrote the first version of the chapter |
132 about parsing. |
136 about parsing. |
133 |
137 |
134 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
138 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
135 chapter and also contributed recipe \ref{rec:named}. |
139 chapter and also contributed the material on @{text NamedThmsFun}. |
136 \end{itemize} |
140 \end{itemize} |
137 |
141 |
138 Please let me know of any omissions. Responsibility for any remaining |
142 Please let me know of any omissions. Responsibility for any remaining |
139 errors lies with me. |
143 errors lies with me.\bigskip |
|
144 |
|
145 {\Large\bf |
|
146 This document is still in the process of being written! All of the |
|
147 text is still under constructions. Sections and |
|
148 chapters that are under \underline{heavy} construction are marked |
|
149 with TBD.} |
|
150 |
|
151 |
|
152 \vfill |
|
153 This document was compiled with:\\ |
|
154 \input{version} |
140 *} |
155 *} |
141 |
156 |
|
157 |
|
158 |
142 end |
159 end |