--- a/doc-src/System/Thy/Sessions.thy Sat Jul 28 21:10:54 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Sat Jul 28 22:01:21 2012 +0200
@@ -194,7 +194,7 @@
\texttt{ROOT} file and an additional catalog file @{verbatim
"etc/sessions"} with further sub-directories (list of lines). Note
that a single \texttt{ROOT} file usually defines many sessions;
- catalogs are are only required for extra scalability and modularity
+ catalogs are only required for extra scalability and modularity
of large libraries.
\medskip The subset of sessions to be managed is selected via
--- a/doc-src/System/Thy/document/Sessions.tex Sat Jul 28 21:10:54 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Sat Jul 28 22:01:21 2012 +0200
@@ -303,7 +303,7 @@
command line. Each such directory may contain a session
\texttt{ROOT} file and an additional catalog file \verb|etc/sessions| with further sub-directories (list of lines). Note
that a single \texttt{ROOT} file usually defines many sessions;
- catalogs are are only required for extra scalability and modularity
+ catalogs are only required for extra scalability and modularity
of large libraries.
\medskip The subset of sessions to be managed is selected via