Part: II
The proof engine

• Chapter 5: Vernacular commands
• Chapter 6: Proof handling
• Chapter 7: Tactics
• Chapter 8: Detailed examples of tactics