Re: [isabelle] Isabelle2013-RC2 available for testing
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”. Don't know if it's on purpose or a bug.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and