8 If your next project requires you to program on the ML-level of Isabelle, |
8 If your next project requires you to program on the ML-level of Isabelle, |
9 then this tutorial is for you. It will guide you through the first steps of |
9 then this tutorial is for you. It will guide you through the first steps of |
10 Isabelle programming, and also explain tricks of the trade. The best way to |
10 Isabelle programming, and also explain tricks of the trade. The best way to |
11 get to know the ML-level of Isabelle is by experimenting with the many code |
11 get to know the ML-level of Isabelle is by experimenting with the many code |
12 examples included in the tutorial. The code is as far as possible checked |
12 examples included in the tutorial. The code is as far as possible checked |
13 against \input{version}. If something does not work, |
13 against the Isabelle code.\footnote{\input{version}} If something does not work, |
14 then please let us know. It is impossible for us to know every environment, |
14 then please let us know. It is impossible for us to know every environment, |
15 operating system or editor in which Isabelle is used. If you have comments, |
15 operating system or editor in which Isabelle is used. If you have comments, |
16 criticism or like to add to the tutorial, please feel free---you are most |
16 criticism or like to add to the tutorial, please feel free---you are most |
17 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
17 welcome! The tutorial is meant to be gentle and comprehensive. To achieve |
18 this we need your feedback. |
18 this we need your feedback. |
135 \item @{text thy} for theories; ML-type: @{ML_type theory} |
135 \item @{text thy} for theories; ML-type: @{ML_type theory} |
136 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
136 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
137 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
137 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
138 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
138 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
139 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
139 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
|
140 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
140 \end{itemize} |
141 \end{itemize} |
141 *} |
142 *} |
142 |
143 |
143 section {* Acknowledgements *} |
144 section {* Acknowledgements *} |
144 |
145 |
151 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
152 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
152 \simpleinductive-package and the code for the @{text |
153 \simpleinductive-package and the code for the @{text |
153 "chunk"}-antiquotation. He also wrote the first version of the chapter |
154 "chunk"}-antiquotation. He also wrote the first version of the chapter |
154 describing the package and has been helpful \emph{beyond measure} with |
155 describing the package and has been helpful \emph{beyond measure} with |
155 answering questions about Isabelle. |
156 answering questions about Isabelle. |
|
157 |
|
158 \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. |
156 |
159 |
157 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
160 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
158 \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. |
161 \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. |
159 He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}. |
162 He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}. |
160 |
163 |