session S = HOL + theories Base T
