[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Embedding TLA+ in Latex

Thank you, that was it!

On Monday, May 6, 2019 at 3:11:54 AM UTC+2, Leslie Lamport wrote:
You are apparently running the Java program TLA.java.  That takes as input a TLA module and produces a typeset version of that module.  You want to run the program TeX.java.  That program takes a LaTeX file containing TLA+ formulas that appear in "tla" environments.  It writes a new version of that file in which, after each such environment, it adds a "tlatex" environment (replacing any existing one) that produces the typeset version of those TLA+ formulas.  The LaTeX file should use the tlatex package.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e6732c16-acc0-481d-800f-5f227f461d27%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.