# HG changeset patch
# User haftmann
# Date 1343505681 -7200
# Node ID 38e225bd53e48b7cd227f341a5a2febcc5eee6b9
# Parent  80ba76b46247bfa082c2e9585bf45ad5fb564f5d
corrected slip

diff -r 80ba76b46247 -r 38e225bd53e4 doc-src/System/Thy/Sessions.thy
--- 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
diff -r 80ba76b46247 -r 38e225bd53e4 doc-src/System/Thy/document/Sessions.tex
--- 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