diff options
Diffstat (limited to 'backends/hol4/primitivesArithScript.sml')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index d251a7cc..fa2f144d 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -68,7 +68,7 @@ Proof rw [LE_EQ_GE] >> sg ‘y <> 0’ >- COOPER_TAC >> qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >> - fs [] >> POP_IGNORE_TAC >> rw [] >- COOPER_TAC >> + fs [] >> pop_ignore_tac >> rw [] >- COOPER_TAC >> fs [NOT_LT_EQ_GE] >> (* Proof by contradiction: assume k < 0 *) spose_not_then ASSUME_TAC >> |