52 and even those can be undone when the proof |
52 and even those can be undone when the proof |
53 script is retracted. As mentioned in the Introduction, we will drop the |
53 script is retracted. As mentioned in the Introduction, we will drop the |
54 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
54 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
55 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
55 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
56 code, rather they indicate what the response is when the code is evaluated. |
56 code, rather they indicate what the response is when the code is evaluated. |
|
57 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf}. |
|
58 The first evaluates the given code, but any effect on the ambient |
|
59 theory is suppressed. The second needs to be used if ML-code is defined |
|
60 inside a proof. For example |
|
61 |
|
62 \begin{isabelle} |
|
63 \isacommand{lemma}~@{text "test:"}\isanewline |
|
64 \isacommand{shows}~@{text [quotes] "True"}\isanewline |
|
65 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial\""}~@{text "\<verbclose>"}\isanewline |
|
66 \isacommand{oops} |
|
67 \end{isabelle} |
|
68 |
|
69 Inside a proof the \isacommand{ML} will generate an error message. |
|
70 However, both commands will not play any role in this tutorial. |
57 |
71 |
58 Once a portion of code is relatively stable, you usually want to export it |
72 Once a portion of code is relatively stable, you usually want to export it |
59 to a separate ML-file. Such files can then be included somewhere inside a |
73 to a separate ML-file. Such files can then be included somewhere inside a |
60 theory by using the command \isacommand{use}. For example |
74 theory by using the command \isacommand{use}. For example |
61 |
75 |