Have you looked at Adam Chlipala's Certified Programming with Dependent Types book? It uses Coq and Proof General. There's an online version: http://adam.chlipala.net/cpdt/