A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving (Logical Methods in Computer Science, 2012)