equal
deleted
inserted
replaced
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. |
98 We use @{text "$"} to indicate that a command needs to be run |
98 We use @{text "$"} to indicate that a command needs to be run |
99 in a Unix-shell, for example |
99 in a Unix-shell, for example: |
100 |
100 |
101 @{text [display] "$ ls -la"} |
101 @{text [display] "$ ls -la"} |
102 |
102 |
103 Pointers to further information and Isabelle files are typeset in |
103 Pointers to further information and Isabelle files are typeset in |
104 italic and highlighted as follows: |
104 italic and highlighted as follows: |