equal
deleted
inserted
replaced
69 All ML-code in this Cookbook is typeset in highlighed boxes, like the following |
69 All ML-code in this Cookbook is typeset in highlighed boxes, like the following |
70 ML-expression. |
70 ML-expression. |
71 |
71 |
72 \begin{isabelle} |
72 \begin{isabelle} |
73 \begin{graybox} |
73 \begin{graybox} |
74 \isa{\isacommand{ML} |
74 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
75 \isacharverbatimopen\isanewline |
|
76 \hspace{5mm}@{ML "3 + 4"}\isanewline |
75 \hspace{5mm}@{ML "3 + 4"}\isanewline |
77 \isacharverbatimclose} |
76 @{text "\<verbclose>"} |
78 \end{graybox} |
77 \end{graybox} |
79 \end{isabelle} |
78 \end{isabelle} |
80 |
79 |
81 This corresponds to how code can be processed inside the interactive |
80 This corresponds to how code can be processed inside the interactive |
82 environment of Isabelle. It is therefore easy to experiment with the code |
81 environment of Isabelle. It is therefore easy to experiment with the code |
83 (which by the way is highly recommended). However, for better readability we |
82 (which by the way is highly recommended). However, for better readability we |
84 will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots |
83 will drop the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write |
85 \isacharverbatimclose} and just write |
|
86 |
84 |
87 |
85 |
88 @{ML [display,gray] "3 + 4"} |
86 @{ML [display,gray] "3 + 4"} |
89 |
87 |
90 for the code above. Whenever appropriate we also show the response the code |
88 for the code above. Whenever appropriate we also show the response the code |