ACL2-PC::RUNES

(macro) print the runes used so far
Major Section:  PROOF-CHECKER-COMMANDS

Example and general form:
runes

This command does not change the proof-checker state. Rather, it simply reports runes that have participated in the interactive proof up to this point.