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 <sven.schneider.pub at gmx.de> 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.