# Re: [isabelle] Reference for Pure

On Sat, 25 Aug 2012, John Munroe 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
``perspective.
`

`As the author of the above slides I am also a little confused about the
``formulations of the questions. Only Larry or Randy can say if this a
``"reasonably sufficient reference".
`

`I made these slides for a 1-day Isabelle tutorial at Place d'Italie in
``Paris, which is the core Coq development group. We had some interesting
``discussions on that day, including the question why "fix" and "assume" are
``not the same thing in Isabelle/Isar, and the underlying Pure framework.
``(Nobody outside the type-theory group actually understood that question.)
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*