<history-command> ::= history [ <number> | all ]
history history 10 history all
LP annotates the history by commenting out erroneous commands, by marking the beginning and end of executed files, by marking the creation of subgoals and the completion of proofs, and by indenting the history to reveal its proof structure.
After a thaw command, LP's current history is replaced by the history that led to the corresponding freeze. Thus a script file provides a record of the commands executed during the current LP session, and the history provides a record of commands that will recreate LP's current state.
Users who want a script that will recreate LP's current state, but who have forgotten to issue a set script command, can issue a set log command instead followed by a history all command to capture the script in the log file.