Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014



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

>
> Also note that a tactic or proof method cannot easily provide
> side-results as warning (or error) by itself, due to the ubiquitious
> backtracking, which was a big thing in Isabelle89.  (Backtracking has
> recently made into Coq 8.5 as well, with similar consequences on
> diagnostic tactics.)
>

--Sven Schneider

Attachment: 0xF0E2AE90.asc
Description: application/pgp-keys



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