[isabelle] Reference for Pure



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.