ProgTutorial/Recipes/CallML.thy
changeset 531 cf7ef23348ed
parent 517 d8c376662bb4
child 542 4b96e3c8b33e
equal deleted inserted replaced
530:aabb4c93a6ed 531:cf7ef23348ed
    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")