diff options
Diffstat (limited to 'backends/hol4/primitivesArithScript.sml')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 6 |
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 *) |