*To*: Stephan Merz <Stephan.Merz at loria.fr>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 01 Mar 2010 09:13:59 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Peter Lammich <peter.lammich at uni-muenster.de>*In-reply-to*: <F39F155E-3841-4C16-8966-CC203C9125A0@loria.fr>*References*: <4B86BBA6.803@uni-muenster.de> <F39F155E-3841-4C16-8966-CC203C9125A0@loria.fr>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Stephan Merz wrote:

I second this request. More precisely, I'd like to be able to annotate a rule such that it is applied by the automatic proof methods only if the first n hypotheses are present in the current proof state. As a simple example, consider bspec, which would make a perfect elimination rule when its two assumptions can be proved by assumption. As others have pointed out, it is not hard to write a tactic that applies a rule only if the first n hypotheses can be proved by assumption, however, I don't know how to make such a tactic work inside auto and friends. Thanks, Stephan

Stephan,

Jeremy

**References**:**[isabelle] Generalized elimination rule?***From:*Peter Lammich

**Re: [isabelle] Generalized elimination rule?***From:*Stephan Merz

- Previous by Date: [isabelle] Anyone like to help?
- Previous by Thread: Re: [isabelle] Generalized elimination rule?
- Next by Thread: [isabelle] MetiTarski 1.3 available
- Cl-isabelle-users February 2010 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