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

Please let me know if more clarification is needed.



On Sun, Aug 26, 2012 at 10:38 AM, Lawrence Paulson <lp15 at> 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> wrote:
>> Hi,
>> I have a question about Pure. Is
>> 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.