From 18550ec15e8ca25770ca6d9a58c9d754d9c9861e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 11 May 2018 18:21:28 +0100
Subject: Add snapshot of HOL4 output for CHERI and RISC-V

---
 .../hol4/lem/hol-lib/lem_maybe_extraScript.sml     | 23 ++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml

(limited to 'snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml')

diff --git a/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml
new file mode 100644
index 00000000..6b04d291
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml
@@ -0,0 +1,23 @@
+(*Generated by Lem from maybe_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_basic_classesTheory lem_maybeTheory lem_assert_extraTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_maybe_extra"
+
+ 
+
+(*open import Basic_classes Maybe Assert_extra*)
+
+(* ----------------------- *)
+(* fromJust                *)
+(* ----------------------- *)
+
+(*val fromJust : forall 'a. Maybe.maybe 'a -> 'a*)
+(*let fromJust op=  match op with | Just v -> v | Nothing -> failwith "fromJust of Nothing" end*)
+
+val _ = export_theory()
+
-- 
cgit v1.2.3