Very often I wish to work in an existing theory script file which begins
with a number of files being opened, e.g.,
open prim_recTheory pairTheory listTheory rich_listTheory;
open combinTheory;
open listLib;
open pred_setTheory pred_setLib;
open numTheory;
open numLib;
open arithmeticTheory;
. . .
But for theories that contain hundreds or thousands of theorems, this
prints out each theorem in full, which can take tens of minutes of my time
while I am waiting to begin work, and theorems that I already know are just
spilling by.
Clearly this is not practical. What do other people do to speed this up, so
you can get into your theory and start work? Is there any way to enter the
defined names of an existing theory, like arithmeticTheory, to the current
ML session without printing all of them, which is what takes such a long
time? I'd like to use something like
open_silently arithmeticTheory;
which would be functionally equivalent to "open", but would print none of
the values it is introducing.
What do people do to get around this problem? Or do they just live with it?
Would "open_silently" have to be added to the Standard ML implementation?
Peter
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
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. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
