equal
deleted
inserted
replaced
87 |
87 |
88 @{ML [display,gray] "3 + 4"} |
88 @{ML [display,gray] "3 + 4"} |
89 |
89 |
90 Whenever appropriate we also show the response the code |
90 Whenever appropriate we also show the response the code |
91 generates when evaluated. This response is prefixed with a |
91 generates when evaluated. This response is prefixed with a |
92 @{text [quotes] ">"} like: |
92 @{text [quotes] ">"}, like: |
93 |
93 |
94 @{ML_response [display,gray] "3 + 4" "7"} |
94 @{ML_response [display,gray] "3 + 4" "7"} |
95 |
95 |
96 The usual user-level commands of Isabelle are written in bold, for |
96 The usual user-level commands of Isabelle are written in bold, for |
97 example \isacommand{lemma}, \isacommand{foobar} and so on. |
97 example \isacommand{lemma}, \isacommand{foobar} and so on. |