equal
deleted
inserted
replaced
36 @{text "\<verbclose>"}\isanewline |
36 @{text "\<verbclose>"}\isanewline |
37 @{text "> 7"}\smallskip |
37 @{text "> 7"}\smallskip |
38 \end{graybox} |
38 \end{graybox} |
39 \end{isabelle} |
39 \end{isabelle} |
40 |
40 |
41 Like normal Isabelle proof scripts, \isacommand{ML}-commands can be |
41 Like normal Isabelle scripts, \isacommand{ML}-commands can be |
42 evaluated by using the advance and undo buttons of your Isabelle |
42 evaluated by using the advance and undo buttons of your Isabelle |
43 environment. The code inside the \isacommand{ML}-command can also contain |
43 environment. The code inside the \isacommand{ML}-command can also contain |
44 value and function bindings, for example |
44 value and function bindings, for example |
45 *} |
45 *} |
46 |
46 |