Michael's Prosper Page

HOL Training materials

Old material converted

• 1. Introduction
• 2. Logic (syntax)
• 3. Logic (primitive basis)
• 4. Overview of ML
• 6. Mechanization of logic
• 8. Forward Proof
• 9. Goal-directed proof (tactics)
• 10. Tacticals. (Removed exposition of resolution tactics, as these are hideous, and not even tacticals in any case.)
• 11. Theorem continuations
• 12. Applications survey (old slides)
• 13. Hardware applications
• 14. Software applications
• 15. Embeddings
• 17. Conversions

New modules

• 5. Using HOL
• 7. Theories in HOL
• 16. Defining data types and functions
• 18. The HOL Library
• ?. Holmake
• ?. The Simplifier
• ?. The Parser
• ?. HolBddLib

Case studies

• Combinatory Logic with HOL script file.

Related links

• Prosper project home-page.