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
