diff --git a/doc/report/applications-screenshots.tex b/doc/report/applications-screenshots.tex index cd4fffd8b70bb13abb588ddabdec29e30db40b42..7ec633b28fdb069043a50f48e0a88ffb4165109a 100644 --- a/doc/report/applications-screenshots.tex +++ b/doc/report/applications-screenshots.tex @@ -27,6 +27,7 @@ \shadowbox{\includegraphics[width=\textwidth]{figs/explore4.png}} \caption{The original source code for a given node in our data set.\\}\label{fig:isrc} \end{subfigure} - \caption{Exploring the Isabelle~export~\cite{uloisabelle} with a rudimentary - web interface.}\label{fig:appss} + \caption{Exploring the Isabelle~export~\cite{uloisabelle} with a + rudimentary web interface. A demo of this tool is available at + \url{https://ulordf4j.mathhub.info}.}\label{fig:appss} \end{figure*} diff --git a/doc/report/implementation.tex b/doc/report/implementation.tex index f2b3f099e825335b455a7737fe9fc72613984811..f930ecc6f471e0794c8856ed6ba3bcd220b7db72 100644 --- a/doc/report/implementation.tex +++ b/doc/report/implementation.tex @@ -325,12 +325,8 @@ of this is easy to deploy using a single Docker Compose file. Our concrete implementation is useful in so far as that we can use it to experiment with ULO data sets. But development also provided -insight about (1)~which components this class of systems requires and -(2)~which problems need to be solved. One topic we discussed at large +insight about (1)~which components this class of system requires and +(2)~which problems need to be solved. One topic we discussed at length is version management. It is easy to dismiss this in these early stages of development, but no question it is something to keep in mind. - -With our stack ready for use, we will now continue with a look at some -interesting applications and queries built on top of this -infrastructure. diff --git a/doc/report/legal.tex b/doc/report/legal.tex index 521d8018da2359b5bc8d679f9091a5a3f630299e..ad5680e082820f16a7ab6f5b62dbf66cd82f0a89 100644 --- a/doc/report/legal.tex +++ b/doc/report/legal.tex @@ -4,7 +4,7 @@ Quellen angefertigt habe und dass die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen - wurde.Alle Ausführungen, die wörtlich oder sinngemäß übernommen + wurde. Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet. \end{otherlanguage*}