The state-and-exception monad that is used by the proof-producing translator for monadic HOL functions.
ml_monadBaseLib.sml: Proof automation for the state-and-exception monad that is supported by the proof-producing monadic translator.
ml_monadBaseScript.sml: Definitions for the state-and-exception monad that is supported by the proof-producing monadic translator.