55 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
55 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
56 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
56 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
57 code, rather they indicate what the response is when the code is evaluated. |
57 code, rather they indicate what the response is when the code is evaluated. |
58 |
58 |
59 Once a portion of code is relatively stable, you usually want to export it |
59 Once a portion of code is relatively stable, you usually want to export it |
60 to a separate ML-file. Such files can then be included in a theory by using |
60 to a separate ML-file. Such files can then be included somewhere inside a |
61 the \isacommand{uses}-command in the header of the theory, like: |
61 theory by using the command \isacommand{use}. For example |
|
62 |
|
63 \begin{center} |
|
64 \begin{tabular}{@ {}l} |
|
65 \isacommand{theory} FirstSteps\\ |
|
66 \isacommand{imports} Main\\ |
|
67 \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\ |
|
68 \isacommand{begin}\\ |
|
69 \ldots\\ |
|
70 \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\ |
|
71 \ldots |
|
72 \end{tabular} |
|
73 \end{center} |
|
74 |
|
75 The \isacommand{uses}-command in the header of the theory is needed in order |
|
76 to indicate the dependency of the theory on the ML-file. Alternatively, the |
|
77 file can be included by just writing in the header |
62 |
78 |
63 \begin{center} |
79 \begin{center} |
64 \begin{tabular}{@ {}l} |
80 \begin{tabular}{@ {}l} |
65 \isacommand{theory} FirstSteps\\ |
81 \isacommand{theory} FirstSteps\\ |
66 \isacommand{imports} Main\\ |
82 \isacommand{imports} Main\\ |
67 \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
83 \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
68 \isacommand{begin}\\ |
84 \isacommand{begin}\\ |
69 \ldots |
85 \ldots |
70 \end{tabular} |
86 \end{tabular} |
71 \end{center} |
87 \end{center} |
72 |
88 |
|
89 Note that no parentheses are given this time. |
73 *} |
90 *} |
74 |
91 |
75 section {* Debugging and Printing\label{sec:printing} *} |
92 section {* Debugging and Printing\label{sec:printing} *} |
76 |
93 |
77 text {* |
94 text {* |
225 commas (map (str_of_thm_no_vars ctxt) thms) *} |
242 commas (map (str_of_thm_no_vars ctxt) thms) *} |
226 |
243 |
227 section {* Combinators\label{sec:combinators} *} |
244 section {* Combinators\label{sec:combinators} *} |
228 |
245 |
229 text {* |
246 text {* |
|
247 (FIXME: Calling convention) |
|
248 |
230 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
249 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
231 the combinators. At first they seem to greatly obstruct the |
250 the combinators. At first they seem to greatly obstruct the |
232 comprehension of the code, but after getting familiar with them, they |
251 comprehension of the code, but after getting familiar with them, they |
233 actually ease the understanding and also the programming. |
252 actually ease the understanding and also the programming. |
234 |
253 |
1614 |
1634 |
1615 ML_val{*structure t = Test(U) *} |
1635 ML_val{*structure t = Test(U) *} |
1616 |
1636 |
1617 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*} |
1637 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*} |
1618 |
1638 |
|
1639 ML {* LocalTheory.restore *} |
|
1640 ML {* LocalTheory.set_group *} |
|
1641 *) |
|
1642 |
1619 section {* Storing Theorems\label{sec:storing} (TBD) *} |
1643 section {* Storing Theorems\label{sec:storing} (TBD) *} |
1620 |
1644 |
1621 text {* @{ML PureThy.add_thms_dynamic} *} |
1645 text {* @{ML PureThy.add_thms_dynamic} *} |
1622 |
1646 |
1623 |
1647 |