This directory contains snapshots of definitions generated from the Sail RISC-V specification for the interactive theorem provers Isabelle/HOL, HOL4, and Coq. These snapshots are provided for convenience, and are not guaranteed to be up-to-date.