Add snapshot of HOL4 output for CHERI and RISC-V

1 files changed, 13 insertions, 0 deletions

diff --git a/snapshots/hol4/README.md b/snapshots/hol4/README.md
new file mode 100644
index 00000000..2a8208c9
--- /dev/null
+++ b/snapshots/hol4/README.md
@@ -0,0 +1,13 @@
+# Snapshot of HOL4 output for Sail CHERI and RISC-V models
+
+These theories are a snapshot of the generated files for the Sail
+CHERI and RISC-V models, translated to HOL4 via Lem.  These are all
+accepted by the current source repository version of HOL4 (from
+roughly 7th May 2018), although we have not done any further testing
+of them yet.
+
+They were generated using the `cheri-mono` branch of Sail, and the
+`hol-with-extra-types` branch of Lem, which currently contain some
+changes that are not yet ready of the main branches of these projects.
+
+11th May 2018.