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.
ml_monadBaseSyntax.sml: ML functions for manipulating HOL terms and types involving the state-and-exception monad defined in ml_monadBase.