Re: [isabelle] Reference for Pure
I wonder whether these concepts are precisely enough defined for your question to be answered in any meaningful way.
On 25 Aug 2012, at 22:57, John Munroe <munddr at gmail.com> wrote:
> 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
> Thanks a lot for your time in advance.
This archive was generated by a fusion of
Pipermail (Mailman edition) and