--- a/src/HOL/Unix/document/root.tex Mon Feb 12 20:45:12 2001 +0100
+++ b/src/HOL/Unix/document/root.tex Mon Feb 12 20:47:19 2001 +0100
@@ -189,7 +189,7 @@
to clean up the situation. In Unix \texttt{root} may perform any file-system
operation without any access control limitations.\footnote{This is the typical
Unix way of handling abnormal situations: while it is easy to run into odd
- cases due to simplistic policies it as well quite easy to get out. There
+ cases due to simplistic policies it is as well quite easy to get out. There
are other well-known systems that make it somewhat harder to get into a fix,
but almost impossible to get out again!}