session S = HOL + theories U
