diff options
Diffstat (limited to 'backends/hol4/primitivesArithScript.sml')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index 2682e507..b7b44b25 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -18,6 +18,7 @@ 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) +(* Miscelleanous *) Theorem int_add_minus_same_eq: ∀ (i j : int). i + j - j = i Proof |