Defopen
A simple event generator that creates a theorem by finding out what a
term simplifies to under some hyp and with some hint.
In contrast to misc/defopener (see defopener), the
reductions carried out by defopen may be less powerful because we only do
simplification (no clausify). However, this seems to produce more compact
expressions than defopener, where the result is formed by combining
several clauses produced from the original term.
General form:
(defopen name term &key (hyp 't)
hint (rule-classes ':rewrite))
See also easy-simplify-term.
