Re: [isabelle] Isar: making implicit intro/elim rules explicit
On 05.01.2011 19:42, David Lazar wrote:
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?
In Proof General, you can enable the "Trace Rules" which causes Isar to
list the rules it considers to do this step. Unfortunately this does not
tell you exactly which rule it chose; but in most cases it is easy to
identify which of these rules was used.
This archive was generated by a fusion of
Pipermail (Mailman edition) and