38 distribution.\footnote{\input{version}} If something does not work, then |
38 distribution.\footnote{\input{version}} If something does not work, then |
39 please let us know. It is impossible for us to know every environment, |
39 please let us know. It is impossible for us to know every environment, |
40 operating system or editor in which Isabelle is used. If you have comments, |
40 operating system or editor in which Isabelle is used. If you have comments, |
41 criticism or like to add to the tutorial, please feel free---you are most |
41 criticism or like to add to the tutorial, please feel free---you are most |
42 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
42 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
43 this we need your feedback. |
43 this we need your help and feedback. |
44 *} |
44 *} |
45 |
45 |
46 section {* Intended Audience and Prior Knowledge *} |
46 section {* Intended Audience and Prior Knowledge *} |
47 |
47 |
48 text {* |
48 text {* |
60 The following documentation about Isabelle programming already exists (and is |
60 The following documentation about Isabelle programming already exists (and is |
61 part of the distribution of Isabelle): |
61 part of the distribution of Isabelle): |
62 |
62 |
63 \begin{description} |
63 \begin{description} |
64 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
64 \item[The Isabelle/Isar Implementation Manual] describes Isabelle |
65 from a high-level perspective, documenting both the underlying |
65 from a high-level perspective, documenting some of the underlying |
66 concepts and some of the interfaces. |
66 concepts and interfaces. |
67 |
67 |
68 \item[The Isabelle Reference Manual] is an older document that used |
68 \item[The Isabelle Reference Manual] is an older document that used |
69 to be the main reference of Isabelle at a time when all proof scripts |
69 to be the main reference of Isabelle at a time when all proof scripts |
70 were written on the ML-level. Many parts of this manual are outdated |
70 were written on the ML-level. Many parts of this manual are outdated |
71 now, but some parts, particularly the chapters on tactics, are still |
71 now, but some parts, particularly the chapters on tactics, are still |
82 things really work. Therefore you should not hesitate to look at the |
82 things really work. Therefore you should not hesitate to look at the |
83 way things are actually implemented. More importantly, it is often |
83 way things are actually implemented. More importantly, it is often |
84 good to look at code that does similar things as you want to do and |
84 good to look at code that does similar things as you want to do and |
85 learn from it. This tutorial contains frequently pointers to the |
85 learn from it. This tutorial contains frequently pointers to the |
86 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
86 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
87 often your best friend while programming with Isabelle, or |
87 often your best friend while programming with Isabelle.\footnote{Or |
88 hypersearch if you program using jEdit under MacOSX. To understand the sources, |
88 hypersearch if you program using jEdit under MacOSX.} To understand the sources, |
89 it is often also necessary to track the change history of a file or |
89 it is often also necessary to track the change history of a file or |
90 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
90 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
91 for Isabelle provides convenient interfaces to query the history of |
91 for Isabelle provides convenient interfaces to query the history of |
92 files and ``change sets''. |
92 files and ``change sets''. |
93 \end{description} |
93 \end{description} |
134 \begin{readmore} |
134 \begin{readmore} |
135 Further information or pointers to files. |
135 Further information or pointers to files. |
136 \end{readmore} |
136 \end{readmore} |
137 |
137 |
138 The pointers to Isabelle files are hyperlinked to the tip of the Mercurial |
138 The pointers to Isabelle files are hyperlinked to the tip of the Mercurial |
139 repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/} |
139 repository at \href{http://isabelle.in.tum.de/repos/isabelle/} |
140 {http://isabelle.in.tum.de/repos/isabelle/}. |
140 {http://isabelle.in.tum.de/repos/isabelle/}, not the latest release |
|
141 of Isabelle. |
141 |
142 |
142 A few exercises are scattered around the text. Their solutions are given |
143 A few exercises are scattered around the text. Their solutions are given |
143 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
144 in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try |
144 to solve the exercises on your own, and then look at the solutions. |
145 to solve the exercises on your own, and then look at the solutions. |
145 *} |
146 *} |
214 people contributed to the text: |
215 people contributed to the text: |
215 |
216 |
216 \begin{itemize} |
217 \begin{itemize} |
217 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
218 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
218 \simpleinductive-package and the code for the @{text |
219 \simpleinductive-package and the code for the @{text |
219 "chunk"}-antiquotation. He also wrote the first version of this chapter |
220 "chunk"}-antiquotation. He also wrote the first version of chapter |
220 describing the package and has been helpful \emph{beyond measure} with |
221 \ref{chp:package} describing this package and has been helpful \emph{beyond |
221 answering questions about Isabelle. |
222 measure} with answering questions about Isabelle. |
222 |
223 |
223 \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. |
224 \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. |
224 |
225 |
225 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
226 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
226 \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} |
227 \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} |
227 and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} |
228 and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} |
228 are by him. |
229 are by him. |
229 |
230 |
230 \item {\bf Lukas Bulwahn} made me aware of the problems with recursive |
231 \item {\bf Lukas Bulwahn} made me aware of a problem with recursive |
231 parsers and contributed exercise \ref{ex:contextfree}. |
232 parsers and contributed exercise \ref{ex:contextfree}. |
232 |
233 |
233 \item {\bf Jeremy Dawson} wrote the first version of the chapter |
234 \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing} |
234 about parsing. |
235 about parsing. |
235 |
236 |
236 \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. |
237 \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. |
237 |
238 |
238 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
239 \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' |
239 chapter and also contributed the material on @{ML_funct Named_Thms}. |
240 chapter and also contributed the material on @{ML_funct Named_Thms}. |
240 |
241 |
241 \item {\bf Christian Sternagel} proofread the tutorial and made |
242 \item {\bf Christian Sternagel} proofread the tutorial and made |
242 many improvemets to the text. |
243 many improvemets to the text. |
243 \end{itemize} |
244 \end{itemize} |