A light-weight integration of automated and interactive theorem proving - Anton Setzer (Mathematical Structures in Computer Science, 2014)