150 simple ML-expression: |
150 simple ML-expression: |
151 |
151 |
152 \begin{isabelle} |
152 \begin{isabelle} |
153 \begin{graybox} |
153 \begin{graybox} |
154 \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline |
154 \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline |
155 \hspace{5mm}@{ML "3 + 4"}\isanewline |
155 \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline |
156 \<open>\<verbclose>\<close> |
156 \<open>\<verbclose>\<close> |
157 \end{graybox} |
157 \end{graybox} |
158 \end{isabelle} |
158 \end{isabelle} |
159 |
159 |
160 These boxes correspond to how code can be processed inside the interactive |
160 These boxes correspond to how code can be processed inside the interactive |
161 environment of Isabelle. It is therefore easy to experiment with the code |
161 environment of Isabelle. It is therefore easy to experiment with the code |
162 that is shown in this tutorial. However, for better readability we will drop |
162 that is shown in this tutorial. However, for better readability we will drop |
163 the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just |
163 the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just |
164 write: |
164 write: |
165 |
165 |
166 @{ML [display,gray] "3 + 4"} |
166 @{ML [display,gray] \<open>3 + 4\<close>} |
167 |
167 |
168 Whenever appropriate we also show the response the code |
168 Whenever appropriate we also show the response the code |
169 generates when evaluated. This response is prefixed with a |
169 generates when evaluated. This response is prefixed with a |
170 @{text [quotes] ">"}, like: |
170 @{text [quotes] ">"}, like: |
171 |
171 |
172 @{ML_matchresult [display,gray] "3 + 4" "7"} |
172 @{ML_matchresult [display,gray] \<open>3 + 4\<close> \<open>7\<close>} |
173 |
173 |
174 The user-level commands of Isabelle (i.e., the non-ML code) are written |
174 The user-level commands of Isabelle (i.e., the non-ML code) are written |
175 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
175 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
176 \isacommand{foobar} and so on). We use \<open>$ \<dots>\<close> to indicate that a |
176 \isacommand{foobar} and so on). We use \<open>$ \<dots>\<close> to indicate that a |
177 command needs to be run in a UNIX-shell, for example: |
177 command needs to be run in a UNIX-shell, for example: |