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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Sun, 5 May 2019 18:11:53 -0700 (PDT)*References*: <09dc02df-fe99-45cf-9200-8d81d736393b@googlegroups.com>

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.

Leslie

-- Leslie

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.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**[tlaplus] Re: Embedding TLA+ in Latex***From:*Jam

**References**:**[tlaplus] Embedding TLA+ in Latex***From:*Jam

- Prev by Date:
**[tlaplus] Embedding TLA+ in Latex** - Next by Date:
**Re: [tlaplus] What is the purpose of THEOREM in AsynchInterface?** - Previous by thread:
**[tlaplus] Embedding TLA+ in Latex** - Next by thread:
**[tlaplus] Re: Embedding TLA+ in Latex** - Index(es):