There is one instance in Extension.thy where you wrote "real ^ n" in a
subsection heading about Urysohn's lemma. That causes an error when
interpreted as LaTeX code. I suggest replacing it with "Euclidean
space", which is more apt in Isabelle anyway, I should think.
There are two more instances in Brouwer_Fixpoint.thy where you wrote
something like "R^n" in text, causing the same error.
Cheers,
Manuel
On 15/06/16 18:19, Lawrence Paulson wrote:
No idea what’s going on here. I did commit a lot of stuff but it works on my
machine. I added a theory, but the addition was committed and I have no
untracked files. If anybody can figure out what’s going on I'd be grateful. I
see it is a document preparation failure, presumably that isn’t being checked
locally for some reason?
Larry
Begin forwarded message:
From: Isabelle/Jenkins <ci@isabelle.systems>
Subject: [Isabelle-ci] Build failure in Isabelle
Date: 15 June 2016 at 17:14:27 BST
To: isabelle...@mail46.informatik.tu-muenchen.de
The Isabelle build failed. See the log at:
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/
_______________________________________________
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
