# Snapshot of HOL4 output for Sail RISC-V model

These theories are a snapshot of the generated files for the Sail RISC-V models
translated to HOL4 via Lem.  They only require HOL4; the necessary Lem library
files are included.

A recent checkout of HOL4 from the repository at
<https://github.com/HOL-Theorem-Prover/HOL/> is required.  This snapshot was
successfully built with commit `86a5bc67f`, for example.  Some older versions
will fail with a Holdep error due to a lexer bug in HOL that has now been
fixed.