diff -r a0b280dd4bc7 -r 520127b708e6 ProgTutorial/Recipes/CallML.thy --- 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: *}