diff options
| author | Son Ho | 2023-01-27 22:25:37 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | a11774e6f501dae120f7a315e32c50981adb3358 (patch) | |
| tree | 26ac68fba00df47fcab294f987d895ca51d213de /backends/hol4/primitivesArithTheory.sig | |
| parent | 3f91598f9c22ea3d1255ce460d843d2abe72d1f0 (diff) | |
Make progress on the standard library for HOL4
Diffstat (limited to 'backends/hol4/primitivesArithTheory.sig')
| -rw-r--r-- | backends/hol4/primitivesArithTheory.sig | 5 |
1 files changed, 5 insertions, 0 deletions
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 |