Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014

There must be some confusion here. No backtracking is needed for rename_tac.

The point is to make your proofs independent of names internally generated by the system. It isn’t wrong if the names you choose turn out to be the same as the internal ones.

Larry Paulson

> On 24 Feb 2015, at 12:49, Sven Schneider < at> wrote:
> Is rename_tac using 'ubiquitious backtracking'? I would not have
> expected rename_tac to be so complex.
> I had a more simple implementation in mind: a tactic-wrapper which
> operates as follows.
> (1) obtain the current list of variables
> (2) apply rename_tac
> (3) obtain the new list of variables
> (4) print a warning if old-list = new-list

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.