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.

  -- Lars





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