[isabelle] Reference for Pure


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