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
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
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
