Re: [isabelle] Reference for Pure

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.