session "HOL+ZF" = HOL + sessions ZF theories ZFC