--- a/ProgTutorial/Recipes/CallML.thy	Tue Jul 20 13:34:44 2010 +0100
+++ b/ProgTutorial/Recipes/CallML.thy	Wed Jul 28 19:09:49 2010 +0200
@@ -16,21 +16,19 @@
 
   To make it clear we mean here calling unverified ML functions from within
   HOL! The motivation is the paradigm of \emph{result checking}: rather than
-  verify some complicated algorithm, have the algorithm produce an easily
-  checkable certificate. For example, rather than verify a primality test,
-  have the test produce a factor of the input as a witness to
-  non-primality. This is only an example, and we ignore the converse
-  certificate, that for primality, although it, too, can be treated in the
-  same manner. 
+  verifying some complicated algorithm, have the algorithm produce an easily
+  checkable certificate. For example, instead of verifying an algorithm for 
+  testing non-primality, have an algorithm that produces a factor as a witness to
+  non-primality. 
 
-  The example we are looking at here is an ML function for finding a factor 
-  of a number. We first declare its type:
+  The algorithm is an ML function finding a factor of a number. We first 
+  declare its type:
 *}
 
 consts factor :: "nat \<Rightarrow> nat"
 
 text{* 
-  Its definition will be given in ML below. But the whole point is that
+  Its definition will be given below in ML. But the whole point is that
   we can prove non-primality via @{const factor}, no matter what its
   actual definition is: 
 *}