Re: [isabelle] successful attempt vs failed to apply initial proof method



On Fri, 18 Mar 2016, Buday Gergely wrote:

And, is there a reference of Output and State messages? The Isabelle/jEdit manual does not seem to contain one.

The GUI panels merely display what certain prover commands produce, so the place to look is the isar-ref manual. For command 'show' it says:

  â @{command "show"}~âa: Ïâ is like @{command "have"}~âa: Ïâ plus a second
  stage to refine some pending sub-goal for each one of the finished result,
  after having been exported into the corresponding context (at the head of
  the sub-proof of this @{command "show"} command).

  To accommodate interactive debugging, resulting rules are printed before
  being applied internally. Even more, interactive execution of @{command
  "show"} predicts potential failure and displays the resulting error as a
  warning beforehand. Watch out for the following message:
  @{verbatim [display] âLocal statement fails to refine any pending goalâ}


	Makarius


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