DATEREC : MEXPR

DATEREC is a top-level command.
Records times used in the following processes:
DIY, Mating Search, Merging Expansion Tree, Proof Transformation.
All times recorded are in seconds.
Internal-runtime includes GC-time.
GC-time is garbage-collecting-time.
I-GC-time is Internal-runtime minus GC-time.
DATEREC also records the values of the flags listed in RECORDFLAGS,
and will offer the user the chance to reset the provability
status of a gwff in the library.
The command format for DATEREC is:

 <n>DATEREC   NAME      TYPE  COMMENT 
"SYMBOL" "LIB-ARGTYPE" "STRING"


The arguments have the following meaning:
NAME : Name of theorem
TYPE : Type of library object
COMMENT : Your choice

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage