[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: higher order sub-term rewriting

> Is it possible to rewrite the goal using the hypothesis. Note that
> such a rewrite is possible within the HOL system, thanks to higher
> order rewriting.

(rewrite -1) is the usual way to rewrite with an antecedent formula.
PVS does some subclass of higher-order matching.  If it doesn't get
this example, send the full thing (M-x dump-pvs-files) and Shankar may
be able to offer an explanation or help.