From a11774e6f501dae120f7a315e32c50981adb3358 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 27 Jan 2023 22:25:37 +0100
Subject: Make progress on the standard library for HOL4

---
 backends/hol4/primitivesArithTheory.sig | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'backends/hol4/primitivesArithTheory.sig')

diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index b2172b7c..e32b49d4 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -3,6 +3,7 @@ sig
   type thm = Thm.thm
   
   (*  Theorems  *)
+    val add_sub_same_eq : thm
     val ge_eq_le : thm
     val gt_eq_lt : thm
     val int_add : thm
@@ -31,6 +32,10 @@ sig
    
    [int_arith] Parent theory of "primitivesArith"
    
+   [add_sub_same_eq]  Theorem
+      
+      ⊢ ∀i j. i + j − j = i
+   
    [ge_eq_le]  Theorem
       
       ⊢ ∀x y. x ≥ y ⇔ y ≤ x
-- 
cgit v1.2.3