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
In fact the kinds of rules printed by
:pl are rewrite rules,
definition rules, and meta rules.