*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Naive question about tactics and Pure*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Tue, 28 Aug 2012 09:23:59 +0900*In-reply-to*: <CAP0k5J4fiPpXUM0avH_z6Z7=8n=ADPpbwpQVLrxVAo0t=se_4g@mail.gmail.com>*References*: <CAP0k5J4fiPpXUM0avH_z6Z7=8n=ADPpbwpQVLrxVAo0t=se_4g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

Hope this makes any sense. cheers chris On 08/28/2012 08:04 AM, John Munroe wrote:

Hi, I have a rather naive question about the use of terminology. AFAIK, tactics are implemented in the meta-level and the meta-level language in Isabelle is Pure. So is it correct to say that "tactics are written in Pure"? Thanks John

**References**:**[isabelle] Naive question about tactics and Pure***From:*John Munroe

- Previous by Date: [isabelle] Naive question about tactics and Pure
- Next by Date: Re: [isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?
- Previous by Thread: [isabelle] Naive question about tactics and Pure
- Next by Thread: [isabelle] Isabelle/jEdit Macros
- Cl-isabelle-users August 2012 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