equal
deleted
inserted
replaced
58 \begin{description} |
58 \begin{description} |
59 \item[The code] is of course the ultimate reference for how |
59 \item[The code] is of course 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. |
63 to learn from that code. The UNIX command @{text "grep -R"} is |
|
64 often your best friend while programming with Isabelle. |
64 \end{description} |
65 \end{description} |
65 |
66 |
66 *} |
67 *} |
67 |
68 |
68 section {* Typographic Conventions *} |
69 section {* Typographic Conventions *} |
69 |
70 |
70 text {* |
71 text {* |
71 |
72 |
72 All ML-code in this tutorial is typeset in highlighted boxes, like the following |
73 All ML-code in this tutorial is typeset in shaded boxes, like the following |
73 ML-expression: |
74 ML-expression: |
74 |
75 |
75 \begin{isabelle} |
76 \begin{isabelle} |
76 \begin{graybox} |
77 \begin{graybox} |
77 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
78 \isacommand{ML}~@{text "\<verbopen>"}\isanewline |
94 |
95 |
95 @{ML_response [display,gray] "3 + 4" "7"} |
96 @{ML_response [display,gray] "3 + 4" "7"} |
96 |
97 |
97 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 |
98 in bold, for example \isacommand{lemma}, \isacommand{apply}, |
99 in bold, for example \isacommand{lemma}, \isacommand{apply}, |
99 \isacommand{foobar} and so on. We use @{text "$"} to indicate that a |
100 \isacommand{foobar} and so on. We use @{text "$ \<dots>"} to indicate that a |
100 command needs to be run in a Unix-shell, for example: |
101 command needs to be run in a Unix-shell, for example: |
101 |
102 |
102 @{text [display] "$ ls -la"} |
103 @{text [display] "$ grep -R ThyOutput *"} |
103 |
104 |
104 Pointers to further information and Isabelle files are typeset in |
105 Pointers to further information and Isabelle files are typeset in |
105 italic and highlighted as follows: |
106 italic and highlighted as follows: |
106 |
107 |
107 \begin{readmore} |
108 \begin{readmore} |