Merge branch 'sail2' into mappings

1 files changed, 45 insertions, 0 deletions

diff --git a/snapshots/isabelle/lib/lem/Lem_assert_extra.thy b/snapshots/isabelle/lib/lem/Lem_assert_extra.thy
new file mode 100644
index 00000000..b56e5a19
--- /dev/null
+++ b/snapshots/isabelle/lib/lem/Lem_assert_extra.thy
@@ -0,0 +1,45 @@
+chapter \<open>Generated by Lem from assert_extra.lem.\<close>
+
+theory "Lem_assert_extra" 
+
+imports 
+ 	 Main
+	 "Lem" 
+
+begin 
+
+
+(*open import {ocaml} `Xstring`*)
+(*open import {hol} `stringTheory` `lemTheory`*)
+(*open import {coq} `Coq.Strings.Ascii` `Coq.Strings.String`*)
+(*open import {isabelle} `$LIB_DIR/Lem`*)
+
+(* ------------------------------------ *)
+(* failing with a proper error message  *)
+(* ------------------------------------ *)
+
+(*val failwith: forall 'a. string -> 'a*)
+
+(* ------------------------------------ *)
+(* failing without an error message     *)
+(* ------------------------------------ *)
+
+(*val fail : forall 'a. 'a*)
+definition fail  :: " 'a "  where 
+     " fail = ( failwith (''fail''))"
+
+
+(* ------------------------------------- *)
+(* assertions                            *)
+(* ------------------------------------- *)
+
+(*val ensure : bool -> string -> unit*)
+definition ensure  :: " bool \<Rightarrow> string \<Rightarrow> unit "  where 
+     " ensure test msg = (
+  if test then
+    () 
+  else
+    failwith msg )"
+
+
+end