Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?
- To: Nils Jähnig <jaehnig at mi.fu-berlin.de>
- Subject: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?
- From: Makarius <makarius at sketis.net>
- Date: Tue, 14 Feb 2012 22:57:15 +0100 (CET)
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <CACU92SCJ-w+1NtskFfsTeg66oj7rkcZni5dG+t_3hfz5Uutn=Q@mail.gmail.com>
- References: <CACU92SCJ-w+1NtskFfsTeg66oj7rkcZni5dG+t_3hfz5Uutn=Q@mail.gmail.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Wed, 25 Jan 2012, Nils Jähnig wrote:
I try to rewrite an apply-style proof into a tactic, for future
Appendix C of the "isar-ref" manual explains the correspondence of ML
tactic expressions and Isar proof methods a little. It was originally
written to help converting old ML proof scripts, which are now obsolete
and hardly ever encountered in recent years, but it also helps in the
The "implementation" manual explains further things about rules and
tactics from the bottom up. The important FOCUS combinator has already
been mentioned -- it is based on Isar structuring principles in ML, and is
able to get rid of most res_inst_tac applications in practice. For plain
thm instantiation you mainly use Thm.instantiate, despite various later
attempts (mostly outdated now) to produce more convenient alternatives.
This archive was generated by a fusion of
Pipermail (Mailman edition) and