Re: [isabelle] Isabelle2013-RC2 available for testing

On Wed, 6 Feb 2013, Yannick Duchêne (Hibou57) wrote:

Le Wed, 06 Feb 2013 00:28:40 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at> a écrit:
I don't know if it's RC related or not,

Another one (I installed RC2 when coming back to Isabelle, and don't remember if it was the same before), also about what's displayed in the output pan, now by the “display_rules” command.

Quick case: “thm conjI” displays “?P ⟹ ?Q ⟹ ?P ∧ ?Q” in the output pan. OK, but “display_rules” displays “?P ⟹ ?Q ⟹ ?P ∧ ?Q” without its name, which is “conjI”.

I have never heard about "display_rules".  Do you mean "print_statement"?

Trying this in Isabelle2013-RC2:

  thm conjI
  print_statement conjI

it looks fine to me. The first case just the proposition of the theorem, and the second with the name of it (guessed according to certain internal "name hints" that happen to work here).


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