1 files changed, 75 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_boolScript.sml b/snapshots/hol4/lem/hol-lib/lem_boolScript.sml
new file mode 100644
index 00000000..5e6aa09f
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_boolScript.sml
@@ -0,0 +1,75 @@
+(*Generated by Lem from bool.lem.*)
+open HolKernel Parse boolLib bossLib;
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_bool"
+
+ 
+
+(* The type bool is hard-coded, so are true and false *)
+
+(* ----------------------- *)
+(* not                     *)
+(* ----------------------- *)
+
+(*val not : bool -> bool*)
+(*let not b=  match b with
+  | true -> false
+  | false -> true
+end*)
+
+(* ----------------------- *)
+(* and                     *)
+(* ----------------------- *)
+
+(*val && [and] : bool -> bool -> bool*)
+(*let && b1 b2=  match (b1, b2) with
+  | (true, true) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* or                      *)
+(* ----------------------- *)
+
+(*val || [or] : bool -> bool -> bool*)
+(*let || b1 b2=  match (b1, b2) with
+  | (false, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* implication             *)
+(* ----------------------- *)
+
+(*val --> [imp] : bool -> bool -> bool*)
+(*let --> b1 b2=  match (b1, b2) with
+  | (true, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* equivalence             *)
+(* ----------------------- *)
+
+(*val <-> [equiv] : bool -> bool -> bool*)
+(*let <-> b1 b2=  match (b1, b2) with
+  | (true, true) -> true
+  | (false, false) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* xor                     *)
+(* ----------------------- *)
+
+(*val xor : bool -> bool -> bool*)
+
+val _ = export_theory()
+