9 text {* |
9 text {* |
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, you are very |
14 know. If you have comments or like to add to the Cookbook, |
15 welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly |
15 feel free--you are very welcome! |
16 updated. |
|
17 |
|
18 *} |
16 *} |
19 |
17 |
20 section {* Intended Audience and Prior Knowledge *} |
18 section {* Intended Audience and Prior Knowledge *} |
21 |
19 |
22 text {* |
20 text {* |
80 \end{isabelle} |
79 \end{isabelle} |
81 |
80 |
82 This corresponds to how code can be processed inside the interactive |
81 This corresponds to how code can be processed inside the interactive |
83 environment of Isabelle. However, for better readability we will drop |
82 environment of Isabelle. However, for better readability we will drop |
84 the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots |
83 the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots |
85 \isacharverbatimclose} and just show |
84 \isacharverbatimclose} and just write |
86 |
85 |
87 @{ML [display,gray] "3 + 4"} |
86 @{ML [display,gray] "3 + 4"} |
88 |
87 |
89 for the code above. Whenever appropriate we show the response of the code |
88 for the code above. Whenever appropriate we also show the response of the code |
90 when evaluated. The response is prefixed with a @{text [quotes] ">"}", like |
89 when evaluated. The response is prefixed with a @{text [quotes] ">"}" like |
91 |
90 |
92 @{ML_response [display,gray] "3 + 4" "7"} |
91 @{ML_response [display,gray] "3 + 4" "7"} |
93 |
92 |
94 Isabelle commands are written in bold. For example \isacommand{lemma}, |
93 Isabelle commands are written in bold, for example \isacommand{lemma}, |
95 \isacommand{foobar} and so on. We use @{text "$"} to indicate a command |
94 \isacommand{foobar} and so on. We use @{text "$"} to indicate that |
96 needs to be run on the Unix-command line, like |
95 a command needs to be run on the Unix-command line, for example |
97 |
96 |
98 @{text [display] "$ ls -la"} |
97 @{text [display] "$ ls -la"} |
99 |
98 |
100 Pointers to further information and files are indicated as follows: |
99 Pointers to further information and Isabelle files are highlighted |
|
100 as follows: |
101 |
101 |
102 \begin{readmore} |
102 \begin{readmore} |
103 Further information. |
103 Further information or pointer to file. |
104 \end{readmore} |
104 \end{readmore} |
105 |
105 |
106 *} |
106 *} |
107 |
107 |
108 |
108 |