By no means I want to exclude the employment of action refinement as a
`how'-step, admitting correctness proofs.  However, this requires the
classification of the refined action as `internal' and falls outside
the scope of this thesis.  Doing so may also be a reason to give up the
convention adopted above.  This would give rise to a completely
different theory.

<P>
In
<B>Rensink:</B> <I>Models and Methods for Action Refinement</I>, Ph.D.
Thesis, University of Twente, 1993,
a mode of action refinement is proposed that I would classify as a
combined `what'- and `how'-step.  Correctness proofs of the
`how'-component of such a refinement step are possible, but relative
to a preorder that is explicitly parametrized with the
`what'-component of the refinement step.