equal
deleted
inserted
replaced
16 \isacommand{imports} Main\\ |
16 \isacommand{imports} Main\\ |
17 \isacommand{begin}\\ |
17 \isacommand{begin}\\ |
18 \ldots |
18 \ldots |
19 \end{tabular} |
19 \end{tabular} |
20 \end{center} |
20 \end{center} |
|
21 |
|
22 We also generally assume you are working with HOL. The given examples might |
|
23 need to be adapted slightly if you work in a different logic. |
21 *} |
24 *} |
22 |
25 |
23 section {* Including ML-Code *} |
26 section {* Including ML-Code *} |
24 |
27 |
25 |
28 |
466 Terms are described in detail in \isccite{sec:terms}. Their |
469 Terms are described in detail in \isccite{sec:terms}. Their |
467 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
470 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
468 \end{readmore} |
471 \end{readmore} |
469 |
472 |
470 Sometimes the internal representation of terms can be surprisingly different |
473 Sometimes the internal representation of terms can be surprisingly different |
471 from what you see at the user level, because the layers of |
474 from what you see at the user-level, because the layers of |
472 parsing/type-checking/pretty printing can be quite elaborate. |
475 parsing/type-checking/pretty printing can be quite elaborate. |
473 |
476 |
474 \begin{exercise} |
477 \begin{exercise} |
475 Look at the internal term representation of the following terms, and |
478 Look at the internal term representation of the following terms, and |
476 find out why they are represented like this: |
479 find out why they are represented like this: |
1083 This code declares a data slot where the theorems are stored, |
1086 This code declares a data slot where the theorems are stored, |
1084 an attribute @{text foo} (with the @{text add} and @{text del} options |
1087 an attribute @{text foo} (with the @{text add} and @{text del} options |
1085 for adding and deleting theorems) and an internal ML interface to retrieve and |
1088 for adding and deleting theorems) and an internal ML interface to retrieve and |
1086 modify the theorems. |
1089 modify the theorems. |
1087 |
1090 |
1088 Furthermore, the facts are made available on the user level under the dynamic |
1091 Furthermore, the facts are made available on the user-level under the dynamic |
1089 fact name @{text foo}. For example you can declare three lemmas to be of the kind |
1092 fact name @{text foo}. For example you can declare three lemmas to be of the kind |
1090 @{text foo} by: |
1093 @{text foo} by: |
1091 *} |
1094 *} |
1092 |
1095 |
1093 lemma rule1[foo]: "A" sorry |
1096 lemma rule1[foo]: "A" sorry |