ACL2-PC::LEMMAS-USED

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

This is just an alias for runes.