Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic? (fwd)

Makarius wrote:
On Fri, 27 Jan 2012, Jeremy Dawson wrote:

For this you want res_inst_tac, described in the Reference manual.
Eg (res_inst_tac [("x", "A")] exI 1)

This probably refers to Isabelle2005, which was the last version with all the old things from Isabelle98 etc. still present. The "Reference manual" is called "Old Reference manual" for quite some years already, and it explicitly says in current Isabelle2011-1:

  Note: this document is part of the earlier Isabelle
  documentation and is mostly outdated.  Fully obsolete parts of the
  original text have already been removed.  The remaining material
  covers some aspects that did not make it into the newer manuals yet.

The "newer manuals" refers mainly to the "Isabelle/Isar Reference Manual and "Isabelle/Isar Implementation Manual".


Yes, I observe that now res_inst_tac requires a proof context argument, and some other changes as well. Makarius is right in guessing that I'm referring to Isabelle2005 - it was when I started to convert all my proofs from Isabelle 2005 to 2007 I seemed to be spending a lot of time on it when I would rather be doing useful work.

I gather things have got worse since then, in terms of incompatibilities between versions of Isabelle and therefore the prospects of users making use of other users' work


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