[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.
Makarius
More information about the isabelle-dev
mailing list