Thanks.
---
Jing
On 2018年1月31日 -0700 AM1:52, Ramana Kumar , wrote:
> Delete the directory in which you installed it.
>
> > On 31 Jan 2018 06:01, "Jing Guo" wrote:
> > > Hi,
> > >
> > > Several months ago I installed HOL and recently I want to uninstall it.
> > > However, after some research I s
[Apologies if you receive multiple copies of this email. Please distribute to
interested parties.]
*** DEADLINE APPROACHING ***
KR18 - Call for Tutorial and Workshop Proposals
** Apologies if you receive multiple copies of this call **
** Please distribute to interested parties **
Hi Yaqing,
Try this below - it returns a minimal thm list, based on the "black box"
technique. But I haven't tested it properly..
Apply it like this:
shrink_rewrite_list REWRITE_CONV [th1;th2;th3;th4] tm;;
Cheers,
Mark.
(* Utils *)
let remove_nth_elem n xs =
let (xs1,xs2) = chop_list
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
---
I might need to forward the solution I got from Mark here as well:
Forwarded Message
Subject:Re: [Hol-info] Tracking lemmas used by REWRITE_CONV
Date: Wed, 31 Jan 2018 15:38:46 +
From: Mark Adams
To: Yaqing Jiang
Hi Yaqing,
Good to know someone's been
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
Delete the directory in which you installed it.
On 31 Jan 2018 06:01, "Jing Guo" wrote:
> Hi,
>
> Several months ago I installed HOL and recently I want to uninstall it.
> However, after some research I still could not find a way, nor it’s
> included in the documentation. So I wondered that what
