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 the 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: |
105 |
105 |
106 \begin{readmore} |
106 \begin{readmore} |
107 Further information or pointer to file. |
107 Further information or pointers to files. |
108 \end{readmore} |
108 \end{readmore} |
109 |
109 |
110 *} |
110 *} |
111 |
111 |
112 |
112 |