Re: [isabelle] Reference for Pure



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
>>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.