ACL2-PC::RUNES

(macro) print the runes (definitions, lemmas, ...) used 
Major Section:  PROOF-CHECKER-COMMANDS


Examples and general forms:
(runes t)   ; print all runes used during this interactive proof
(runes nil) ; print all runes used by the most recent command
(runes)     ; same as (runes nil)
runes       ; same as (runes nil)

This command does not change the proof-checker state. Rather, it simply reports runes (see rune) that have participated in the interactive proof.

Note that (runes nil) will show the runes used by the most recent primitive or macro command (as displayed by :comm).