session S = HOL + theories M
