PL

print the rules whose top function symbol is the given name
Major Section:  HISTORY

Examples:
:pl foo ; prints the rewrite rules that rewrite some call of foo

Pl takes one argument, a function symbol, and displays the lemmas that rewrite some term whose top function symbol is the given one. Note that names of macros are not relevant here; for example, for the rules about + you should give the command :pl binary-+.

In fact the kinds of rules printed by :pl are rewrite rules, definition rules, and meta rules.