Add snapshot of HOL4 output for CHERI and RISC-V

1 files changed, 16 insertions, 0 deletions

diff --git a/snapshots/hol4/lem/hol-lib/lem_pervasives_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_pervasives_extraScript.sml
new file mode 100644
index 00000000..33ccd627
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_pervasives_extraScript.sml
@@ -0,0 +1,16 @@
+(*Generated by Lem from pervasives_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasivesTheory lem_function_extraTheory lem_maybe_extraTheory lem_map_extraTheory lem_num_extraTheory lem_set_extraTheory lem_set_helpersTheory lem_list_extraTheory lem_string_extraTheory lem_assert_extraTheory lem_show_extraTheory lem_machine_wordTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_pervasives_extra"
+
+ 
+
+(*include import Pervasives*) 
+(*include import Function_extra Maybe_extra Map_extra Num_extra Set_extra Set_helpers List_extra String_extra Assert_extra Show_extra Machine_word*)
+val _ = export_theory()
+