*To*: Sven Schneider <sven.schneider.pub at gmx.de>*Subject*: Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014*From*: Makarius <makarius at sketis.net>*Date*: Tue, 24 Feb 2015 14:18:47 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <54EC7346.8020406@gmx.de>*References*: <54DE10B0.4040207@gmx.de> <5AF069CB-BFB5-4721-A070-8A764DD68913@cam.ac.uk> <54E73DCB.2080902@gmx.de> <54E7431A.2050401@in.tum.de> <54E7510E.5090604@gmx.de> <alpine.LNX.2.00.1502231552501.56408@lxbroy10.informatik.tu-muenchen.de> <54EC7346.8020406@gmx.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 24 Feb 2015, Sven Schneider 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 Then rename_tac could be replaced everywhere by the wrapper-tactic..

From the concrete information exposed so far, I am not yet convinced that

So just the standard questions: * What are typical remaining applications of rename_tac? * Is it feasible to dispose it eventually, e.g. after Eisbach has been properly established. Makarius

**References**:**[isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Sven Schneider

**Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Larry Paulson

**Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Sven Schneider

**Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Dmitriy Traytel

**Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Sven Schneider

**Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Makarius

**Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014***From:*Sven Schneider

- Previous by Date: Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014
- Next by Date: Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
- Previous by Thread: Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014
- Next by Thread: [isabelle] The difference between /\ , â and -> , =>
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list