# HG changeset patch
# User wenzelm
# Date 1249394986 -7200
# Node ID a99e58e043ee16fc30cc34b7de1b5cc20c1072ec
# Parent  8185d3bfcbf19b002dddb7240f1fde0fc24384c9
spelling;

diff -r 8185d3bfcbf1 -r a99e58e043ee doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Tue Aug 04 15:59:57 2009 +0200
+++ b/doc-src/System/Thy/Basics.thy	Tue Aug 04 16:09:46 2009 +0200
@@ -81,7 +81,7 @@
   links are admissible, but a plain copy of the @{"file"
   "$ISABELLE_HOME/bin"} files will not work!
 
-  \item The file @{"file" "$ISABELLE_HOME/etc/settings"} ist run as a
+  \item The file @{"file" "$ISABELLE_HOME/etc/settings"} is run as a
   @{executable_ref bash} shell script with the auto-export option for
   variables enabled.
   
diff -r 8185d3bfcbf1 -r a99e58e043ee doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Tue Aug 04 15:59:57 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Tue Aug 04 16:09:46 2009 +0200
@@ -100,7 +100,7 @@
   executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility.  Symbolic
   links are admissible, but a plain copy of the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} files will not work!
 
-  \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} ist run as a
+  \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} is run as a
   \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
   variables enabled.