diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index 3da1423b..b5d9918e 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -9,8 +9,26 @@ open boolTheory arithmeticTheory integerTheory intLib listTheory To be used in conjunction with {!pop_assum} for instance. *) -fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC +fun ignore_tac (_ : thm) : tactic = ALL_TAC -val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC +val pop_ignore_tac = pop_assum ignore_tac + +(* TODO: no exfalso tactic?? *) +val ex_falso : tactic = + SUBGOAL_THEN âFâ (fn th => ASSUME_TAC th >> fs[]) + +fun qspec_assume x th = qspec_then x assume_tac th +fun qspecl_assume xl th = qspecl_then xl assume_tac th +fun first_qspec_assume x = first_assum (qspec_assume x) +fun first_qspecl_assume xl = first_assum (qspecl_assume xl) + + + +val cooper_tac = COOPER_TAC +val pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC + +(* Dependent rewrites *) +val dep_pure_once_rewrite_tac = dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC +val dep_pure_rewrite_tac = dep_rewrite.DEP_PURE_REWRITE_TAC end |