28 The easiest and quickest way to include code in a theory is |
28 The easiest and quickest way to include code in a theory is |
29 by using the \isacommand{ML}-command. For example\smallskip |
29 by using the \isacommand{ML}-command. For example\smallskip |
30 |
30 |
31 \begin{isabelle} |
31 \begin{isabelle} |
32 \begin{graybox} |
32 \begin{graybox} |
33 \isa{\isacommand{ML} |
33 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
34 \isacharverbatimopen\isanewline |
|
35 \hspace{5mm}@{ML "3 + 4"}\isanewline |
34 \hspace{5mm}@{ML "3 + 4"}\isanewline |
36 \isacharverbatimclose\isanewline |
35 @{text "\<verbclose>"}\isanewline |
37 @{text "> 7"}\smallskip} |
36 @{text "> 7"}\smallskip |
38 \end{graybox} |
37 \end{graybox} |
39 \end{isabelle} |
38 \end{isabelle} |
40 |
39 |
41 Like ``normal'' Isabelle proof scripts, |
40 Like ``normal'' Isabelle proof scripts, |
42 \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of |
41 \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of |
43 your Isabelle environment. The code inside the \isacommand{ML}-command |
42 your Isabelle environment. The code inside the \isacommand{ML}-command |
44 can also contain value and function bindings, and even those can be |
43 can also contain value and function bindings, and even those can be |
45 undone when the proof script is retracted. As mentioned earlier, we will |
44 undone when the proof script is retracted. As mentioned earlier, we will |
46 drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
45 drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} |
47 whenever we show code. |
46 whenever we show code. |
48 |
47 |
49 Once a portion of code is relatively stable, one usually wants to |
48 Once a portion of code is relatively stable, one usually wants to |
50 export it to a separate ML-file. Such files can then be included in a |
49 export it to a separate ML-file. Such files can then be included in a |
51 theory by using \isacommand{uses} in the header of the theory, like |
50 theory by using \isacommand{uses} in the header of the theory, like |