I have used today (possibly for the first time) the not a member of symbol in ProofPower HOL and find that it causes an error in pdflatex.
The definition in ProofPower.sty is:
\def\PrIO{\MMM{\not\in}}
which doesn't work (not in my environment), but:
\def\PrIO{\MMM{\notin}}
works fine.
Roger Jones
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
