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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to