[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