I actually never tried it because I thought it was
some
command-line-based thing that output TeX files or some similar
1980's-era thing, and I'd have to use some random tla2ps program
to get useful output from it.
i forgot to mention one more thing: this is what i mean by NOTEEDIT
being ignored: many people are not informed what it really is or does.
and very few people don't recommend NOTEEDIT to the newbyes.
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com