I am working on a paper about a proof procedure and realised that
I was about to write something rather specific to ProofPower.
In ProofPower, the rewriting conversions and tactics treat
free variables on the left-hand side of the equations you are
rewriting with as constants and will only instanti
HI Rob,
I think it would be pretty easy. REWR_CONV and its M-N counterpart
HO_REWR_CONV are built from REWR_CONV0 which takes a "part_match"
function which actually determines how the lhs of the rewrite rule is
matched.
Type variables occurring in the hypotheses of the rewrite rule will not be
As Konrad said, we have two flavours of rewriter. The FREEZE_THEN thm_tactical
can also be used to automate the "trick" whereby free variables get "frozen" in
assumptions. See
http://hol.sourceforge.net/kananaskis-10-helpdocs/help/Docfiles/HTML/Tactic.FREEZE_THEN.html
for documentation. This
