equal
deleted
inserted
replaced
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 Isabelle commands are written in bold, for example \isacommand{lemma}, |
96 The usual user-level commands of Isabelle are written in bold, for |
97 \isacommand{foobar} and so on. We use @{text "$"} to indicate that |
97 example \isacommand{lemma}, \isacommand{foobar} and so on. |
98 a command needs to be run in the Unix-shell, for example |
98 We use @{text "$"} to indicate that a command needs to be run |
|
99 in the Unix-shell, for example |
99 |
100 |
100 @{text [display] "$ ls -la"} |
101 @{text [display] "$ ls -la"} |
101 |
102 |
102 Pointers to further information and Isabelle files are typeset in |
103 Pointers to further information and Isabelle files are typeset in |
103 italic and highlighted as follows: |
104 italic and highlighted as follows: |