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:
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