Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014

On Fri, 20 Feb 2015, Sven Schneider wrote:

(*) Is it possible to adapt rename_tac s.t. it produces a warning if it has not altered the state?

In really ancient times, the former goal stack package of the ML toplevel used to issue such a warning for arbitrary tactic applications; thus it had the above effect for rename_tac. The built-in warning was later discontinued for the Isar proof state management, because it was unclear what "not altered" means.

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

After so many years with old-style tactic emulations in Isar (like rename_tac, rule_tac, erule_tac etc.) it might be time to investigate possibilities to live without them. Recent developments around the Eisbach proof method language could allow to remove these old artifacts eventually.


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