[isabelle] printing of \/ in subgoals



I'm puzzled that in the ProofGeneral front-end, I enjoy so much, the \<or> (well the \/ xsymbol) is only displayed for the term, but not the proof-state window for the lemma below. The subgoal that processing the lemma displays shows me "A B = B A" (no \/). Once a lemma is proved, it's displayed with the correct \/ signs.

  term "A \<or> B = B \<or> A"
  lemma "A \<or> B = B \<or> A"

  Proof (Prove): Step 0
  Fixed Variables: A, B
  Goal (Lemma, 1 Subgoal):
    A B = B A                           <---- missing \/
    1. A B = B A

Any idea how I can get the system to display the \/ character in the subgoal also?

I'm using XEmacs 21.4.15, XSymbols 4.5.1 on OS X 10.4.2 using Apples X Windows server.

Thanks,
- Reto







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