family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies