hol-light-materials Contents An overview of HOL Light HOL Light Setup 1. How-to Use or update assumptions in HOL Light Use rewrite tactics well Write your own tactic Debug a proof and tactic Prove 'trivial' goals 2. More Details OCaml data structure of HOL Light How does tactic work? HOL Light vs. Coq comparison 3. Examples and Exercises exercises: exercises for HOL Light s2n-bignum-examples: examples for proving assembly programs in s2n-bignum 4. Other Online Materials Tutorial HOL Light: an overview Reference Manual (pdf, html) Very Quick Reference (pdf, txt) Misc