		Search-engine friendly clone of the ACL2 documentation.

Ubt

Undo the commands back through a command descriptor

See undo for an introduction to undoing commands.

Examples:
:ubt :max      ; undo back through the most recent command
               ; (which just means undo the most recent command)
:ubt :x        ; same as :ubt :max
:u             ; same as :ubt :max with no questions asked
:ubt fn        ; undo back through the introduction of fn
               ; (including all the other events in fn's block)
:ubt 5         ; undo back through the fifth command executed
:ubt (:max -4) ; undo back through the most recent five commands
:ubt (:x -4)   ; undo back through the most recent five commands

See command-descriptor.

Ubt takes one argument, a command descriptor, and undoes the commands from :max (aka :x) through the one described. See command-descriptor. Pbt will print the commands that ubt will undo. :Oops will undo the undo. See oops.

Ubt can cause errors but not queries. To get queries as well, see ubt?. To get neither errors nor queries, see ubt!..

It is important to remember that a command may create several events. That is, the command that introduces fn1 may also introduce fn2. Undoing the command that created either of these will undo them both. The events created by a command constitute the command's ``block'' and we can only undo entire blocks. Use pcb to print the command block of a command if you wish to see what will be lost by undoing the command.

Ubt will not undo into ``prehistory''. :Ubt 1 will undo all of your commands. But :ubt -5 will cause an error, warning you that :ubt cannot undo system initialization.

See u for how to undo just the latest command. See ubu, ubu!, and ubu? for how to undo back up to, but not including, the current command.