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

*From*: Jam <wawrzynchonewicz@xxxxxxxxx>*Date*: Tue, 21 May 2019 08:08:57 -0700 (PDT)*References*: <09dc02df-fe99-45cf-9200-8d81d736393b@googlegroups.com> <d3c758ab-2859-47bf-9bae-67f261a734e1@googlegroups.com>

Thank you, that was it!

On Monday, May 6, 2019 at 3:11:54 AM UTC+2, Leslie Lamport wrote:

-- 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.

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.

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.

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

**[tlaplus] Re: Embedding TLA+ in Latex***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] Re: how to updating state and return in a definition** - Next by Date:
**[tlaplus] Applicability of TLA+ to the design of electronic circuits and systems?** - Previous by thread:
**[tlaplus] Re: Embedding TLA+ in Latex** - Next by thread:
**[tlaplus] Embedding TLA+ in LaTeX** - Index(es):