--- 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.
--- 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.