Dear Michael,Thanks for your reply, I managed to solve the problem. As a
complementary question, I wonder if HOL4 can use more than one core for its
computations.
Regards,Hamed Nemati
On Sunday, July 24, 2016 5:39 AM, "michael.norr...@data61.csiro.au"
<michael.norr...@data61.csiro.au> wrote:
#yiv7118188152 -- filtered {panose-1:0 0 0 0 0 0 0 0 0 0;}#yiv7118188152
filtered {font-family:Calibri;panose-1:2 15 5 2 2 2 4 3 2 4;}#yiv7118188152
filtered {font-family:HelveticaNeue;}#yiv7118188152 p.yiv7118188152MsoNormal,
#yiv7118188152 li.yiv7118188152MsoNormal, #yiv7118188152
div.yiv7118188152MsoNormal
{margin:0cm;margin-bottom:.0001pt;font-size:12.0pt;}#yiv7118188152 a:link,
#yiv7118188152 span.yiv7118188152MsoHyperlink
{color:#0563C1;text-decoration:underline;}#yiv7118188152 a:visited,
#yiv7118188152 span.yiv7118188152MsoHyperlinkFollowed
{color:#954F72;text-decoration:underline;}#yiv7118188152
span.yiv7118188152EmailStyle17
{font-family:Calibri;color:windowtext;}#yiv7118188152 span.yiv7118188152msoIns
{text-decoration:underline;color:teal;}#yiv7118188152
.yiv7118188152MsoChpDefault {font-size:10.0pt;}#yiv7118188152 filtered
{margin:72.0pt 72.0pt 72.0pt 72.0pt;}#yiv7118188152
div.yiv7118188152WordSection1 {}#yiv7118188152 One approach would be to define
constants that do the abbreviation for you. Then you should recast the
theorems/definitions that EVAL is using to also use those new constants. I'm
afraid there isn't any code already around that automatically detects repeated
sub-terms, so you'd have to write some custom SML to get exactly the behaviour
you want. Michael From: hamed nemati <hn_nemati1...@yahoo.com>
Reply-To: hamed nemati <hn_nemati1...@yahoo.com>
Date: Sunday, 24 July 2016 at 02:59
To: HOL-info List <hol-info@lists.sourceforge.net>
Subject: [Hol-info] EVAL(tac conv rule) Dear All, I would be very grateful
if someone can help me with the following issue, When I am applying
(RESTR_) EVAL(TAC/ CONV / RULE etc.) to evaluate a term I get a very huge
result which has sub-terms repeat several times inside. Is there any smarter
version of EVAL(tac conv rule) which avoids expanding the same sub-terms
repeatedly by for example abbreviating them. This would decrease evaluation
time and make the evaluated term much shorter. Regards, Hamed Nemati
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports.http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
