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 yahoo.fr> 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).


	Makarius


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