equal
deleted
inserted
replaced
92 @{text "\<verbclose>"} |
92 @{text "\<verbclose>"} |
93 \end{graybox} |
93 \end{graybox} |
94 \end{isabelle} |
94 \end{isabelle} |
95 |
95 |
96 These boxes correspond to how code can be processed inside the interactive |
96 These boxes correspond to how code can be processed inside the interactive |
97 environment of Isabelle. It is therefore easy to experiment with what is |
97 environment of Isabelle. It is therefore easy to experiment with the code |
98 displayed. However, for better readability we will drop the enclosing |
98 that is given in this tutorial. However, for better readability we will drop |
99 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write: |
99 the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just |
100 |
100 write: |
101 |
101 |
102 @{ML [display,gray] "3 + 4"} |
102 @{ML [display,gray] "3 + 4"} |
103 |
103 |
104 Whenever appropriate we also show the response the code |
104 Whenever appropriate we also show the response the code |
105 generates when evaluated. This response is prefixed with a |
105 generates when evaluated. This response is prefixed with a |
216 about parsing. |
216 about parsing. |
217 |
217 |
218 \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. |
218 \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. |
219 |
219 |
220 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
220 \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' |
221 chapter and also contributed the material on @{ML_functor Named_Thms}. |
221 chapter and also contributed the material on @{ML_funct Named_Thms}. |
222 |
222 |
223 \item {\bf Christian Sternagel} proofread the tutorial and made |
223 \item {\bf Christian Sternagel} proofread the tutorial and made |
224 many improvemets to the text. |
224 many improvemets to the text. |
225 \end{itemize} |
225 \end{itemize} |
226 |
226 |