Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic? (fwd)
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
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and