The HOL System
TUTORIAL

University of Cambridge

DSTO

SRI International

• Preface
  • Getting started
• Acknowledgements
• Getting and Installing HOL
  • Getting HOL
  • The info-hol mailing list
  • Installing HOL
• Introduction to ML
  • How to interact with ML
• The HOL Logic
  • Overview of higher order logic
  • Terms
  • Exceptions
• Euclid's theorem
  • Divisibility
  • Primality
  • Existence of prime factors
  • Euclid's theorem
  • Turning the script into a theory
  • Summary
• Introduction to Proof with HOL
  • Forward proof
  • Rewriting
• Goal Oriented Proof: Tactics and Tacticals
  • Using tactics to prove theorems
  • Tacticals
  • Some tactics built into HOL
• Example: a simple parity checker
  • Introduction
  • Specification
  • Implementation
  • Verification
  • Exercises
• More examples
• References

This document was tranlated from L^AT_EX by H^EV^EA and H^AC^HA.