On 31/01/18 10:37, Yaqing Jiang wrote:
> Thanks for the information. I'll check this in HOL Light.
You are welcome.
Please address replies to messages in a mailing list to the mailing
list, unless there is some special reason for not to.
signature.asc
Description: OpenPGP digital signature
---
On 31/01/18 06:49, Yaqing Jiang wrote:
> Anyone knows if there is a simple way of finding out which theorems were
> actually applied?
In HOL4 you can do “set_trace "simplifier" 2;” (or an higher value) to
display information about how the term is being rewritten by simpLib (it
is a more general fa
Hi Yaqing,
I could enhance my Tactician tool to do this sort of thing. In fact, a
new release is long overdue, so I'll try to find the time to do this
soon (but am too busy in the next few weeks).
But you say you're looking for a quick patch. One approach would be to
apply the original con
Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a term, not
all the theorems in th1,th2,... are used.
Anyone knows if there is a simple way of finding out which theorems were
actually applied?
I know there are methods that tracking the entire dependencies of a
proven theorem, bu
