*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Reference for Pure*From*: John Munroe <munddr at gmail.com>*Date*: Sun, 26 Aug 2012 11:04:20 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1C3A769D-13BF-4BD9-BAAC-622175909FC7@cam.ac.uk>*References*: <CAP0k5J687naon10QTbxDqtpy_ie+v3SmBXW0OsCGsqFn1ydKzg@mail.gmail.com> <1C3A769D-13BF-4BD9-BAAC-622175909FC7@cam.ac.uk>

Sorry, I'll try to clarify clarify my question. For example, if the transformation is to negate each axiom in a theory or the transformation is to make some syntactic changes, e.g., rename certain term to something else, then is it still expressible in Pure? I've just found http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf and it seems that there isn't appropriate syntax at least for the latter. If that's the case, does that mean these transformations would sit in a separate meta-level in the logic hierarchy -- between Pure and the object-logic? Please let me know if more clarification is needed. Thanks John On Sun, Aug 26, 2012 at 10:38 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > I wonder whether these concepts are precisely enough defined for your question to be answered in any meaningful way. > > Larry Paulson > > > On 25 Aug 2012, at 22:57, John Munroe <munddr at gmail.com> wrote: > >> Hi, >> >> I have a question about Pure. Is >> http://www.lri.fr/~wenzel/Isabelle2011-Paris/pure.pdf a reasonably >> sufficient reference for summarising the primitives of Pure? If so, >> suppose my function requires something richer than those presented on >> page 2, e.g., theory manipulations, does that mean I'm actually >> working in a separate meta-logic (one that sits between Pure and the >> object-logic)? That is, I'm actually using Pure to encode theory >> manipulations, so it's an object-logic when viewed from Pure's >> perspective. >> >> Thanks a lot for your time in advance. >> >> John >> >

**Follow-Ups**:**Re: [isabelle] Reference for Pure***From:*Lawrence Paulson

**References**:**[isabelle] Reference for Pure***From:*John Munroe

**Re: [isabelle] Reference for Pure***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Reference for Pure
- Next by Date: Re: [isabelle] Reference for Pure
- Previous by Thread: Re: [isabelle] Reference for Pure
- Next by Thread: Re: [isabelle] Reference for Pure
- 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