Hybrid Interactive Theorem Proving Using Nuprl and HOL.

Amy P. Felty, Douglas J. Howe

Browse the full CADE paper archive.