Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014
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..
Ubiquitious backtracking means you participate in a general situation of
any number of results -- in a compostion of lazy functions that produce
them. This means that in general, warnings or errors don't work without
extra thought and extra machinery.
(The problem is similar in parse translations: sometimes people emit
warnings there, but it merely means some confusing messages pop up out of
nothing, without relation to the actual result.)
A canonical way to get the above effect is to make rename_tac strict, in
the sense that it simply fails on vacous renaming. Thus it would behave
like the "simp" method in that respect, in contrast to the internal
From the concrete information exposed so far, I am not yet convinced that
it is worth the while to revisit such ancient tactical relics in the Isar
method name space at all.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and