diff -r 6de6bc551a8b -r b66a4305749c thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Mon Feb 07 01:12:36 2022 +0000
+++ b/thys2/Paper/document/root.tex	Mon Feb 07 14:22:08 2022 +0000
@@ -88,7 +88,7 @@
   paper we describe a variant of Sulzmann and Lu's algorithm: Our
   algorithm is a recursive functional program, whereas Sulzmann
   and Lu's version involves a fixpoint construction. We \textit{(i)}
-  prove in Isabelle/HOL that our program is correct and generates
+  prove in Isabelle/HOL that our algorithm is correct and generates
   unique POSIX values; we also \textit{(ii)} establish a finite
   bound for the size of the derivatives.