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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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