[isabelle-dev] NEWS: generated code as proper theory export
Makarius
makarius at sketis.net
Mon Feb 4 17:41:09 CET 2019
On 01/02/2019 15:30, Lars Hupel wrote:
>
> – Sturm_Sequences produces some extra LaTeX documentation. The generated
> PDF is even committed to the AFP.
>
>> * no generated files in the repository (these are not sources but
>> results from sources)
See now
changeset: 10104:394951259923
user: wenzelm
date: Mon Feb 04 16:42:52 2019 +0100
files: thys/Sturm_Sequences/ROOT
thys/Sturm_Sequences/document/build
thys/Sturm_Sequences/document/root_userguide.tex
thys/Sturm_Sequences/guide/Makefile thys/Sturm_Sequences/guide/guide.pdf
thys/Sturm_Sequences/guide/guide.tex
thys/Sturm_Sequences/guide/isabelle.eps
thys/Sturm_Sequences/guide/isabelle.pdf
description:
proper Isabelle document setup, without generated files in the repository;
It means that the document will also show up in the generated HTML,
similar to the userguide in AFP/Collections.
Makarius
More information about the isabelle-dev
mailing list