• 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-prehistory

      Undo the commands back through the last reset-prehistory event

      See undo for an introduction to undoing commands.

      This command is only used to eliminate a reset-prehistory event. If your most recent reset-prehistory event does not have a flag argument of t, then :ubt-prehistory undoes all command back through, and including, that reset-prehistory event.