equal
deleted
inserted
replaced
52 easily emulated in HOL. In fact, we could even call some external software |
52 easily emulated in HOL. In fact, we could even call some external software |
53 from ML, e.g.\ a computer algebra system. |
53 from ML, e.g.\ a computer algebra system. |
54 |
54 |
55 It should be noted, however, that in this example you need to import the |
55 It should be noted, however, that in this example you need to import the |
56 theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to |
56 theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to |
57 be implemented by the ML-type @{text "int"}. Thus the ML implementation of |
57 be implemented by the ML-type @{text "int"}. |
|
58 |
|
59 \begin{graybox}\small |
|
60 \isacommand{theory}~@{text CallML}\\ |
|
61 \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Efficient_Nat"}\\ |
|
62 ... |
|
63 \end{graybox} |
|
64 |
|
65 |
|
66 Thus the ML implementation of |
58 @{const factor} must be and is of type @{text "int -> int"}. Now it is time |
67 @{const factor} must be and is of type @{text "int -> int"}. Now it is time |
59 to connect the two levels: |
68 to connect the two levels: |
60 *} |
69 *} |
61 |
70 |
62 code_const factor (SML "factor") |
71 code_const factor (SML "factor") |