# [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)
qed
The proof can be reduced to:
lemma "A --> A"
proof
assume a: "A"
show "A" by (rule a)
qed
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.
Thanks,
David

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