summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesArithScript.sml
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/primitivesArithScript.sml')
-rw-r--r--backends/hol4/primitivesArithScript.sml6
1 files changed, 6 insertions, 0 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index 6c96c908..2682e507 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -18,6 +18,12 @@ val le_eq_ge = store_thm("le_eq_ge", “!(x y : int). x <= y <=> y >= x”, coop
val gt_eq_lt = store_thm("gt_eq_lt", “!(x y : int). x > y <=> y < x”, cooper_tac)
val lt_eq_gt = store_thm("lt_eq_gt", “!(x y : int). x < y <=> y > x”, cooper_tac)
+Theorem int_add_minus_same_eq:
+ ∀ (i j : int). i + j - j = i
+Proof
+ int_tac
+QED
+
(*
* We generate and save an induction theorem for positive integers
*)