54 \end{description} |
54 \end{description} |
55 |
55 |
56 Then of course there is: |
56 Then of course there is: |
57 |
57 |
58 \begin{description} |
58 \begin{description} |
59 \item[The code] is of course the ultimate reference for how |
59 \item[The code.] Which is the ultimate reference for how |
60 things really work. Therefore you should not hesitate to look at the |
60 things really work. Therefore you should not hesitate to look at the |
61 way things are actually implemented. More importantly, it is often |
61 way things are actually implemented. More importantly, it is often |
62 good to look at code that does similar things as you want to do and |
62 good to look at code that does similar things as you want to do and |
63 to learn from that code. The UNIX command @{text "grep -R"} is |
63 learn from it. The UNIX command @{text "grep -R"} is |
64 often your best friend while programming with Isabelle. |
64 often your best friend while programming with Isabelle. |
65 \end{description} |
65 \end{description} |
66 |
66 |
67 *} |
67 *} |
68 |
68 |
79 \hspace{5mm}@{ML "3 + 4"}\isanewline |
79 \hspace{5mm}@{ML "3 + 4"}\isanewline |
80 @{text "\<verbclose>"} |
80 @{text "\<verbclose>"} |
81 \end{graybox} |
81 \end{graybox} |
82 \end{isabelle} |
82 \end{isabelle} |
83 |
83 |
84 These boxes corresponds to how code can be processed inside the interactive |
84 These boxes correspond to how code can be processed inside the interactive |
85 environment of Isabelle. It is therefore easy to experiment with what is |
85 environment of Isabelle. It is therefore easy to experiment with what is |
86 displayed. However, for better readability we will drop the enclosing |
86 displayed. However, for better readability we will drop the enclosing |
87 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write: |
87 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write: |
88 |
88 |
89 |
89 |
93 generates when evaluated. This response is prefixed with a |
93 generates when evaluated. This response is prefixed with a |
94 @{text [quotes] ">"}, like: |
94 @{text [quotes] ">"}, like: |
95 |
95 |
96 @{ML_response [display,gray] "3 + 4" "7"} |
96 @{ML_response [display,gray] "3 + 4" "7"} |
97 |
97 |
98 The user-level commands of Isabelle (i.e.~the non-ML code) are written |
98 The user-level commands of Isabelle (i.e., the non-ML code) are written |
99 in bold, for example \isacommand{lemma}, \isacommand{apply}, |
99 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
100 \isacommand{foobar} and so on. We use @{text "$ \<dots>"} to indicate that a |
100 \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a |
101 command needs to be run in a Unix-shell, for example: |
101 command needs to be run in a Unix-shell, for example: |
102 |
102 |
103 @{text [display] "$ grep -R ThyOutput *"} |
103 @{text [display] "$ grep -R ThyOutput *"} |
104 |
104 |
105 Pointers to further information and Isabelle files are typeset in |
105 Pointers to further information and Isabelle files are typeset in |
106 italic and highlighted as follows: |
106 \textit{italic} and highlighted as follows: |
107 |
107 |
108 \begin{readmore} |
108 \begin{readmore} |
109 Further information or pointers to files. |
109 Further information or pointers to files. |
110 \end{readmore} |
110 \end{readmore} |
111 |
111 |