diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml new file mode 100644 index 00000000..3da1423b --- /dev/null +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -0,0 +1,16 @@ +(* Base tactics for the primitives library *) +structure primitivesBaseTacLib = +struct + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory + +(* Ignore a theorem. + + To be used in conjunction with {!pop_assum} for instance. + *) +fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC + +val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC + +end |