10 The purpose of this Cookbook is to guide the reader through the first steps |
10 The purpose of this Cookbook is to guide the reader through the first steps |
11 of Isabelle programming, and to explain tricks of the trade. The code |
11 of Isabelle programming, and to explain tricks of the trade. The code |
12 provided in the Cookbook is as far as possible checked against recent |
12 provided in the Cookbook is as far as possible checked against recent |
13 versions of Isabelle. If something does not work, then please let us |
13 versions of Isabelle. If something does not work, then please let us |
14 know. If you have comments or like to add to the Cookbook, |
14 know. If you have comments or like to add to the Cookbook, |
15 feel free--you are very welcome! |
15 feel free---you are most welcome! |
16 *} |
16 *} |
17 |
17 |
18 section {* Intended Audience and Prior Knowledge *} |
18 section {* Intended Audience and Prior Knowledge *} |
19 |
19 |
20 text {* |
20 text {* |
76 \hspace{5mm}@{ML "3 + 4"}\isanewline |
76 \hspace{5mm}@{ML "3 + 4"}\isanewline |
77 \isacharverbatimclose} |
77 \isacharverbatimclose} |
78 \end{graybox} |
78 \end{graybox} |
79 \end{isabelle} |
79 \end{isabelle} |
80 |
80 |
81 This corresponds to how code can be processed inside the interactive |
81 This corresponds to how code can be processed inside the interactive |
82 environment of Isabelle. However, for better readability we will drop |
82 environment of Isabelle. It is therefore easy to experiment with the code |
83 the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots |
83 (which by the way is highly recommended). However, for better readability we |
|
84 will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots |
84 \isacharverbatimclose} and just write |
85 \isacharverbatimclose} and just write |
|
86 |
85 |
87 |
86 @{ML [display,gray] "3 + 4"} |
88 @{ML [display,gray] "3 + 4"} |
87 |
89 |
88 for the code above. Whenever appropriate we also show the response of the code |
90 for the code above. Whenever appropriate we also show the response the code |
89 when evaluated. The response is prefixed with a @{text [quotes] ">"}" like |
91 generates when evaluated. This response is prefixed with a |
|
92 @{text [quotes] ">"} like |
90 |
93 |
91 @{ML_response [display,gray] "3 + 4" "7"} |
94 @{ML_response [display,gray] "3 + 4" "7"} |
92 |
95 |
93 Isabelle commands are written in bold, for example \isacommand{lemma}, |
96 The usual Isabelle commands are written in bold, for example \isacommand{lemma}, |
94 \isacommand{foobar} and so on. We use @{text "$"} to indicate that |
97 \isacommand{foobar} and so on. We use @{text "$"} to indicate that |
95 a command needs to be run on the Unix-command line, for example |
98 a command needs to be run on the Unix-command line, for example |
96 |
99 |
97 @{text [display] "$ ls -la"} |
100 @{text [display] "$ ls -la"} |
98 |
101 |
99 Pointers to further information and Isabelle files are highlighted |
102 Pointers to further information and Isabelle files are given |
100 as follows: |
103 as follows: |
101 |
104 |
102 \begin{readmore} |
105 \begin{readmore} |
103 Further information or pointer to file. |
106 Further information or pointer to file. |
104 \end{readmore} |
107 \end{readmore} |