[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
I'm using XEmacs 21.4.15, XSymbols 4.5.1 on OS X 10.4.2 using Apples
X Windows server.
This archive was generated by a fusion of
Pipermail (Mailman edition) and