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



I did forget to reply.
it helped. with the name i found the tactic and its syntax. the right way
to use it is

res_inst_tac @{context} [ ( (x,0) , "A" ) ] exI 1


which was convenient for me, as i don't have a term, but a string, which is
easier to manipulate, if you're not yet on good terms with terms.

Nils


2012/2/15 Jeremy Dawson <jeremy at rsise.anu.edu.au>

> 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".
>>
>>
>>    Makarius
>>
>>  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
>
> Jeremy
>
>
>
>
>




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