*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Giving a name to a tactics-expression*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Fri, 19 Feb 2010 06:23:16 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4B7D850E.2080204@uni-muenster.de>*References*: <4B7D7698.40207@uni-muenster.de> <4B7D850E.2080204@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Peter Lammich wrote:

Peter Lammich schrieb:Is there a way to give a short name to a complex tactic-expression. Ihave, e.g., the following pattern that I frequently use.apply (((erule (1) lemma1)+)?,erule lemma2,simp)+Trying to translate it to ML, I cannot find any ML-tactics equivalentfor "erule (1)". There is only etac, but this seems to have no number ofadditional premises.

http://tphols.in.tum.de/idw.html

Good luck! Rafal Kolanski.

**References**:**[isabelle] Giving a name to a tactics-expression***From:*Peter Lammich

**Re: [isabelle] Giving a name to a tactics-expression***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Giving a name to a tactics-expression
- Next by Date: Re: [isabelle] Giving a name to a tactics-expression
- Previous by Thread: Re: [isabelle] Giving a name to a tactics-expression
- Next by Thread: Re: [isabelle] Giving a name to a tactics-expression
- 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