:pl are rewrite rules,
definition rules, and meta rules.
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.