DATEREC : MEXPRDATEREC 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