equal
deleted
inserted
replaced
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, feel free---you are most welcome! The tutorial is meant to be |
18 gentle and comprehensive. |
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 |
23 text {* |
23 text {* |
92 generates when evaluated. This response is prefixed with a |
92 generates when evaluated. This response is prefixed with a |
93 @{text [quotes] ">"}, like: |
93 @{text [quotes] ">"}, like: |
94 |
94 |
95 @{ML_response [display,gray] "3 + 4" "7"} |
95 @{ML_response [display,gray] "3 + 4" "7"} |
96 |
96 |
97 The usual user-level commands of Isabelle are written in bold, for |
97 The user-level commands of Isabelle (i.e.~the non-ML code) are written |
98 example \isacommand{lemma}, \isacommand{foobar} and so on. |
98 in bold, for example \isacommand{lemma}, \isacommand{apply}, |
99 We use @{text "$"} to indicate that a command needs to be run |
99 \isacommand{foobar} and so on. We use @{text "$"} to indicate that a |
100 in a Unix-shell, for example: |
100 command needs to be run in a Unix-shell, for example: |
101 |
101 |
102 @{text [display] "$ ls -la"} |
102 @{text [display] "$ ls -la"} |
103 |
103 |
104 Pointers to further information and Isabelle files are typeset in |
104 Pointers to further information and Isabelle files are typeset in |
105 italic and highlighted as follows: |
105 italic and highlighted as follows: |
112 |
112 |
113 section {* Acknowledgements *} |
113 section {* Acknowledgements *} |
114 |
114 |
115 text {* |
115 text {* |
116 Financial support for this tutorial was provided by the German |
116 Financial support for this tutorial was provided by the German |
117 Research Council (DFG) under grant number URB 165/5-1. |
117 Research Council (DFG) under grant number URB 165/5-1. The following |
|
118 people contributed: |
118 |
119 |
119 \begin{itemize} |
120 \begin{itemize} |
120 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
121 \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the |
121 \simpleinductive-package and the code for the @{text "chunk"}-antiquotation. He also wrote the first |
122 \simpleinductive-package and the code for the @{text |
122 version of the chapter describing the package and has be |
123 "chunk"}-antiquotation. He also wrote the first version of the chapter |
123 helpful \emph{beyond measure} with answering questions about Isabelle. |
124 describing the package and has been helpful \emph{beyond measure} with |
|
125 answering questions about Isabelle. |
124 |
126 |
125 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
127 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
126 \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. |
128 \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. |
127 |
129 |
128 \item {\bf Jeremy Dawson} wrote the first version of the chapter |
130 \item {\bf Jeremy Dawson} wrote the first version of the chapter |