Re: [isabelle] from thy to latex

On 28/02/17 18:47, Michel via Cl-isabelle-users wrote:
> How to obtain a tex file from a thy file ?
> Under JEdit, I have tried "Plugins>Code2HTML>Latex current buffer" but
> the tex file obtained contains many definitions of the same commands.

Isabelle document preparation is done on the command-line, without the
Prover IDE.

Short version:

  isabelle mkroot -d Test && isabelle build -D Test

Long version: read chapter 3 of the "system" manual (e.g. from
Documentation panel).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.