diff options
| author | Son Ho | 2023-01-26 08:52:16 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | af587522a71574f6022cd5c99942ced6063e9e3b (patch) | |
| tree | bc08b4310b40c8e7fe9efbd972b8bb13042935c0 /backends/hol4/primitivesBaseTacLib.sml | |
| parent | e1cba64611fe04dd87f7c54eb92fad2d2a9be4f9 (diff) | |
Use lower case in the names for the HOL4 backend
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index 0368ee9a..75df3015 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -5,6 +5,9 @@ struct open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory +(* Remark: below, we also have conversions *) +val gsym = GSYM + (* Ignore a theorem. To be used in conjunction with {!pop_assum} for instance. @@ -13,12 +16,15 @@ fun ignore_tac (_ : thm) : tactic = ALL_TAC val pop_ignore_tac = pop_assum ignore_tac -val try_tac = TRY - (* TODO: no exfalso tactic?? *) -val ex_falso : tactic = +val exfalso : tactic = SUBGOAL_THEN âFâ (fn th => ASSUME_TAC th >> fs[]) +val try_tac = TRY +val first_tac = FIRST +val map_first = MAP_FIRST +val fail_tac = FAIL_TAC + 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) |