*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic? (fwd)*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 15 Feb 2012 10:40:41 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1202142351370.1945@macbroy22.informatik.tu-muenchen.de>*References*: <alpine.LNX.2.00.1202142351370.1945@macbroy22.informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

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 withall the old things from Isabelle98 etc. still present. The "Referencemanual" 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 ReferenceManual and "Isabelle/Isar Implementation Manual".Makarius

Jeremy

**Follow-Ups**:**[isabelle] Isabelle incompatibilities***From:*Makarius

**References**:

- Previous by Date: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic? (fwd)
- Next by Date: [isabelle] Isabelle incompatibilities
- Previous by Thread: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic? (fwd)
- Next by Thread: [isabelle] Isabelle incompatibilities
- Cl-isabelle-users February 2012 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