session S = HOL + theories Y
