		Search-engine friendly clone of the ACL2 documentation.

Ubu

Undo the commands back up to (not including) a command descriptor

See undo for an introduction to undoing commands.

Examples:
:ubu :x-3      ; undo the last three commands (same as :ubt :x-2)
:ubu (:x -3)   ; same as above
:ubu fn        ; undo back up to, but not including the introduction of fn
               ; (so fn will continue to be defined)
:ubu 5         ; undo back up to, but not including, the fifth command
               ; executed (leaving the first five commands in place)

See command-descriptor.

Ubu takes one argument, a command descriptor, and undoes the commands from :max (aka :x) up to, but not including, the indicated command. See command-descriptor.

Ubu can cause errors. To avoid these, see ubu!.

For appropriate queries to be made, see ubu?.

Also see ubt, which is similar but also undoes the indicated command. As for :ubt, :oops will undo the undo (see oops) and ubu will not undo into ``prehistory''.

See u for how to undo just the latest command, and see ubt, ubt!, and ubt? for how to undo back through (that is, including) the current command.