[isabelle] Isar: making implicit intro/elim rules explicit

The paper "A Tutorial Introduction to Structured Isar Proofs" has the
following simple example:

lemma "A --> A"
proof (rule impI)
  assume a: "A"
  show "A" by (rule a)

The proof can be reduced to:

lemma "A --> A"
  assume a: "A"
  show "A" by (rule a)

by making the proof method "(rule impI)" implicit.  As stated in the
paper, the "proof" command is short for "proof (rule elim-rules
intro-rules)", where "elim-rules" and "intro-rules" are selected by
Isar automatically based on the context.  Is there a way to see Isar's
choices for "elim-rules" and "intro-rules" (and also "." and "..")?
In other words, is there a way to turn a proof that uses implicit
proof methods into a proof where all the proof methods are explicit?

I can see how implicit proof methods make proofs easier to read and
write, but seeing these things explicitly would be very helpful in
learning Isar.


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