• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
        • Pl
        • Command
        • Puff
        • Pc
        • Ld-history
        • Oops
        • Extend-pe-table
        • Ubt
        • Puff*
        • Ubi
        • Undo
        • Make-termination-theorem
        • Pe
        • Command-descriptor
        • Gthm
        • Reset-prehistory
        • Formula
        • Pr
        • Pcb
        • Ubu
        • Disable-ubt
        • Pl2
        • Enter-boot-strap-mode
        • Pbt
          • 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!
        • Parallelism
        • Programming
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • History

    Pbt

    Print the commands back through a command descriptor

    Examples:
    :pbt :max      ; print back through the most recent command
    :pbt :x        ; print back through the most recent command
    :pbt fn        ; print back through the introduction of fn
    :pbt 5         ; print back through the fifth command executed
    :pbt (:x -4)   ; print back through the most recent five commands

    See command-descriptor.

    Pbt takes one argument, a command descriptor, and prints the commands from :max (aka :x) through the one described. See command-descriptor for a description of what a command descriptor is. See pc for a description of the format used to display commands. Pbt will print the commands that ubt will undo.