session S = HOL + theories A B C D
