• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
        • Pl
        • Command
        • Puff
        • Pc
        • Ld-history
        • Oops
        • Extend-pe-table
        • Ubt
        • Puff*
        • Ubi
        • Pe
        • Undo
          • Ubt
          • Ubu
          • Ubt!
            • U
            • Ubu!
            • Ubu?
            • Ubt?
            • Ubt-prehistory
          • Make-termination-theorem
          • Command-descriptor
          • Reset-prehistory
          • Gthm
          • Formula
          • Pr
          • Pcb
          • Ubu
          • Disable-ubt
          • Pl2
          • Pbt
          • Enter-boot-strap-mode
          • Reset-kill-ring
          • Ubt!
            • U
            • Tthm
            • Pf
            • Ubu!
            • Pr!
            • Pcs
            • Pcb!
            • Get-command-sequence
            • Exit-boot-strap-mode
            • Ubu?
            • Ubt?
            • Ep-
            • Ubt-prehistory
            • Tau-database
            • Ep
            • Pe!
          • Programming
          • Operational-semantics
          • Real
          • Start-here
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • History
      • Undo

      Ubt!

      Undo commands, without a query or an error

      See undo for an introduction to undoing commands.

      Example:
      :ubt! :x-4

      The keyword command :ubt! is the same as :ubt, but with a guarantee that it is ``error-free.'' More precisely, the value returned by :ubt! will always be of the form (mv nil val state). Note that :ubt! will not print error messages.

      :Oops will undo the last :ubt!. See ubt, ubt?, ubu!, ubu, ubu?, and u.