*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Giving a name to a tactics-expression*From*: Makarius <makarius at sketis.net>*Date*: Fri, 19 Feb 2010 10:52:10 +0100 (CET)*In-reply-to*: <4B7DECC2.6090906@rsise.anu.edu.au>*References*: <4B7D7698.40207@uni-muenster.de> <4B7DECC2.6090906@rsise.anu.edu.au>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 19 Feb 2010, Jeremy Dawson wrote:

Basically, it seems that methods can be combined in these sorts of ways, butit is hidden in the source code, which is essentially undocumented.erule isMethod.erule ; val it = fn : int -> Thm.thm list -> Method.method combining methods usesMethod.Then ;val it = fn : Method.text list -> Method.textMethod.Try ;val it = fn : Method.text -> Method.textMethod.Repeat1 ;val it = fn : Method.text -> Method.text You then have to work out how to get between a method and a Method.text One way would useMethod.Basic ;val it = fn : (ProofContext.context -> Method.method) -> Method.text

Incidentally all the above code is Isabelle2007, some of it also changedto make some functions visible.

Makarius

**Follow-Ups**:**Re: [isabelle] Giving a name to a tactics-expression***From:*Jeremy Dawson

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

**Re: [isabelle] Giving a name to a tactics-expression***From:*Jeremy Dawson

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