refactoring: merger atomic with prover in BasicIsabelle