On 29/09/17 03:20, Ramana Kumar wrote:
> One possible variation on your must_prove might be the following:
> qmatch_rename_tac {term quotation} >- {tactic}
Good idea. Thanks you.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
On 27/09/17 05:29, Chun Tian (binghe) wrote:
> Honestly speaking, I like those abbreviated “power” tactics, such that
"fs"
> for FULL_SIMP_TAC, "rfs" for REV_FULL_SIMP_TAC, etc., but using all
tactics
> in smaller cases (e.g. strip_tac/STRIP_TAC) doesn't make much sense to me,
> because it makes
Honestly speaking, I like those abbreviated “power” tactics, such that "fs"
for FULL_SIMP_TAC, "rfs" for REV_FULL_SIMP_TAC, etc., but using all tactics
in smaller cases (e.g. strip_tac/STRIP_TAC) doesn't make much sense to me,
because it makes me harder to distinguish between the "inner" and
In case it's not obvious, the place to make feature requests is here:
https://github.com/HOL-Theorem-Prover/HOL/issues
Implementation detail: I would guess you could get per-theorem timing by
setting the "default prover" to one that does timing, similar to how the
--fast option sets it to one
There is no nice way to do this on a per-theorem basis, though I can imagine an
option to Holmake that would turn on some sort of logging like this. Can you
make a feature request please?
You do get per-theory timing information emitted at the end of each script
file, and you could see this
