70 \end{quote} |
70 \end{quote} |
71 |
71 |
72 However, both commands will only play minor roles in this tutorial (we most of |
72 However, both commands will only play minor roles in this tutorial (we most of |
73 the time make sure that the ML-code is defined outside proofs). |
73 the time make sure that the ML-code is defined outside proofs). |
74 |
74 |
75 |
75 |
76 |
|
77 |
|
78 Once a portion of code is relatively stable, you usually want to export it |
76 Once a portion of code is relatively stable, you usually want to export it |
79 to a separate ML-file. Such files can then be included somewhere inside a |
77 to a separate ML-file. Such files can then be included somewhere inside a |
80 theory by using the command \isacommand{use}. For example |
78 theory by using the command \isacommand{ML\_file}. For example |
81 |
79 |
82 \begin{quote} |
80 \begin{quote} |
83 \begin{tabular}{@ {}l} |
81 \begin{tabular}{@ {}l} |
84 \isacommand{theory} First\_Steps\\ |
82 \isacommand{theory} First\_Steps\\ |
85 \isacommand{imports} Main\\ |
83 \isacommand{imports} Main\\ |
86 \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\ |
|
87 \isacommand{begin}\\ |
84 \isacommand{begin}\\ |
88 \ldots\\ |
85 \ldots\\ |
89 \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\ |
86 \isacommand{ML\_file}~@{text "\"file_to_be_included.ML\""}\\ |
90 \ldots |
87 \ldots |
91 \end{tabular} |
88 \end{tabular} |
92 \end{quote} |
89 \end{quote} |
93 |
|
94 The \isacommand{uses}-command in the header of the theory is needed in order |
|
95 to indicate the dependency of the theory on the ML-file. Alternatively, the |
|
96 file can be included by just writing in the header |
|
97 |
|
98 \begin{quote} |
|
99 \begin{tabular}{@ {}l} |
|
100 \isacommand{theory} First\_Steps\\ |
|
101 \isacommand{imports} Main\\ |
|
102 \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
|
103 \isacommand{begin}\\ |
|
104 \ldots |
|
105 \end{tabular} |
|
106 \end{quote} |
|
107 |
|
108 Note that no parentheses are given in this case. Note also that the included |
|
109 ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle |
|
110 is unable to record all file dependencies, which is a nuisance if you have |
|
111 to track down errors. |
|
112 *} |
90 *} |
113 |
91 |
114 section {* Printing and Debugging\label{sec:printing} *} |
92 section {* Printing and Debugging\label{sec:printing} *} |
115 |
93 |
116 text {* |
94 text {* |