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