[isabelle-dev] Building the IsarImplementation Manual on 9fc17f9ccd6c

Makarius makarius at sketis.net
Wed Mar 28 11:35:59 CEST 2012

On Wed, 28 Mar 2012, Lukas Bulwahn wrote:

> I cannot build the IsarImplementation Manual on 9fc17f9ccd6c:
> Maybe some latest change broke the document generation.

See now Isabelle/b9b2e183e94d.

We still don't have fully automatic doc tests, so it has to be checked 
manually.  Doing that I've found another drop-out:

*** Unknown fact "numeral_0_eq_0" (line 28 of "~~/doc-src/TutorialI/Types/Numbers.thy")
*** The error(s) above occurred in document antiquotation: "Pure.thm" (line 28 of "~~/doc-src/TutorialI/Types/Numbers.thy")
*** At command "text" (line 27 of "~~/doc-src/TutorialI/Types/Numbers.thy")

Brian should know what to do here.


More information about the isabelle-dev mailing list