The mechanization in Higher Order Logic of a general- purpose operational semantics for programming languages is described. The mechanization allows the sound derivation of Dijkstra-style axiomatic semantics. A small ...