Re: [isabelle] Reference for Pure

On Sat, 25 Aug 2012, John Munroe wrote:

I have a question about Pure. Is 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.)


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