[isabelle] typo in isar-ref?



I'm trying to understand exactly what Isabelle/HOL proofs are at a low
level so I have a chance at understanding how to extract OpenTheory proofs
for Isabelle/HOL theories.

On page 30 (pdf page 41) of isar-ref.pdf the example of goal oriented
reasoning is either wrong or too confusing for me. In particular the third
application of the resolution seems to introduce the wrong subgoal, and
then the application of assumption seems magical.

While I'm asking, in the description of resolution and assumption rules on
the top half of that page, is it assumed that any subgoal can be worked on,
or does it have to be the leftmost one? If the former is true it would be
better if the example demonstrated that.

Finally, if anyone knows about the proof terms that can be recorded, I'd
love to eventually know exactly how (or whether) they relate to which parts
of Isabelle reasoning. Do they perhaps encode resolution and assumption
applications? Anything else?




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