# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1340181738 -3600
# Node ID cf7ef23348edb3ff7578e57f94230508e20e5c23
# Parent  aabb4c93a6edc1591fa1940e57826b3526b158f5
tuned

diff -r aabb4c93a6ed -r cf7ef23348ed ProgTutorial/Recipes/CallML.thy
--- a/ProgTutorial/Recipes/CallML.thy	Wed Jun 20 08:53:38 2012 +0100
+++ b/ProgTutorial/Recipes/CallML.thy	Wed Jun 20 09:42:18 2012 +0100
@@ -54,7 +54,16 @@
 
   It should be noted, however, that in this example you need to import the
   theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to
-  be implemented by the ML-type @{text "int"}. Thus the ML implementation of
+  be implemented by the ML-type @{text "int"}. 
+
+  \begin{graybox}\small
+  \isacommand{theory}~@{text CallML}\\
+  \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Efficient_Nat"}\\
+  ...
+  \end{graybox}
+
+
+  Thus the ML implementation of
   @{const factor} must be and is of type @{text "int -> int"}. Now it is time
   to connect the two levels:
 *}
diff -r aabb4c93a6ed -r cf7ef23348ed progtutorial.pdf
Binary file progtutorial.pdf has changed