GoKawiilJohn Harrison and Juneyoung Lee publish a new HOL Light quick-start tutorial
John Harrison and Juneyoung Lee have released a tutorial intended as an easier on-ramp to the HOL Light theorem prover than its existing manual. The guide walks new users through installation, including options for Windows users via Windows Subsystem for Linux or Cygwin, followed by a graded set of worked examples. It is presented as a supplement to, not a replacement for, the standard HOL Light manual.