24 |
24 |
25 chapter {* First Steps *} |
25 chapter {* First Steps *} |
26 |
26 |
27 |
27 |
28 text {* |
28 text {* |
29 Isabelle programming is done Standard ML, however it often uses an |
29 Isabelle programming is done in Standard ML, however ML-code for Isabelle often |
30 antiquotation mehanism to refer to the logical context of Isabelle. |
30 includes antiquotations to refer to the logical context of Isabelle. |
31 The ML-code that one writes is, just like lemmas and proofs in Isabelle, |
31 Just like lemmas and proofs, code in Isabelle is part of a |
32 part of a theory. If you want to follow the code written in this |
32 theory. If you want to follow the code written in this chapter, we |
33 chapter, we assume you are working inside the theory defined as |
33 assume you are working inside the theory defined by |
34 |
34 |
|
35 \begin{center} |
35 \begin{tabular}{@ {}l} |
36 \begin{tabular}{@ {}l} |
36 \isacommand{theory} CookBook\\ |
37 \isacommand{theory} CookBook\\ |
37 \isacommand{imports} Main\\ |
38 \isacommand{imports} Main\\ |
38 \isacommand{begin}\\ |
39 \isacommand{begin}\\ |
|
40 \ldots |
39 \end{tabular} |
41 \end{tabular} |
40 |
42 \end{center} |
41 |
43 |
42 The easiest and quickest way to include code in a theory is |
44 The easiest and quickest way to include code in a theory is |
43 by using the \isacommand{ML} command. For example |
45 by using the \isacommand{ML} command. For example |
44 *} |
46 *} |
45 |
47 |
46 ML {* |
48 ML {* |
47 3 + 4 |
49 3 + 4 |
48 *} |
50 *} |
49 |
51 |
50 text {* |
52 text {* |
51 The expression inside \isacommand{ML} commands is emmediately evaluated |
53 The expression inside \isacommand{ML} commands is immediately evaluated, |
52 like ``normal'' proof scripts by using the advance and retreat buttons of |
54 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of |
53 your Isabelle environment. The code inside the \isacommand{ML} command |
55 your Isabelle environment. The code inside the \isacommand{ML} command |
54 can also contain value- and function bindings. \marginpar{\tiny FIXME can one undo them like |
56 can also contain value- and function bindings, on which the undo operation |
55 Isabelle lemmas/proofs - probably not} |
57 does not have any effect. |
56 *} |
58 *} |
57 |
59 |
58 section {* Antiquotations *} |
60 section {* Antiquotations *} |
59 |
61 |
60 text {* |
62 text {* |