# HG changeset patch
# User wenzelm
# Date 925751015 -7200
# Node ID 66c941ea1f01900e307a413c980aec9d49b5cf27
# Parent  b38bc78d9a9d6abe14b6c7650fdd9eb0551582fb
tuned;

diff -r b38bc78d9a9d -r 66c941ea1f01 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Mon May 03 18:35:48 1999 +0200
+++ b/doc-src/Ref/goals.tex	Mon May 03 19:03:35 1999 +0200
@@ -309,7 +309,7 @@
 \end{ttdescription}
 
 \goodbreak
-\noindent{\it Error indications for \texttt{back}:}\par\nobreak
+\noindent{\it Error indications for {\tt back}:}\par\nobreak
 \begin{itemize}
 \item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
   means \texttt{back} found a non-empty branch point, but that it contained
diff -r b38bc78d9a9d -r 66c941ea1f01 doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Mon May 03 18:35:48 1999 +0200
+++ b/doc-src/Ref/introduction.tex	Mon May 03 19:03:35 1999 +0200
@@ -145,7 +145,7 @@
 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
 expanded appropriately.  Note that \texttt{\~\relax} abbreviates
 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
-\texttt{\$ISABELLE_HOME}.
+\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.
 
 
 \section{Reading theories}\label{sec:intro-theories}
@@ -177,16 +177,16 @@
 \item[\ttindexbold{the_context}();] obtains the current theory context, or
   raises an error if absent.
   
-\item[\ttindexbold{theory} $name$;] retrieves the theory called $name$ from
+\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
   the internal database of loaded theories, raising an error if absent.
   
-\item[\ttindexbold{use_thy} $name$;] reads theory $name$ from the file system,
-  looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML}; also
-  makes sure that all parent theories are loaded as well.  In case some older
-  versions have already been present, \texttt{use_thy} only tries to reload
-  $name$ itself, but is content with any version of its parents.
+\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
+  system, looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML};
+  also makes sure that all parent theories are loaded as well.  In case some
+  older versions have already been present, \texttt{use_thy} only tries to
+  reload $name$ itself, but is content with any version of its parents.
   
-\item[\ttindexbold{time_use_thy} $name$;] same as \texttt{use_thy}, but
+\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
   reports the time taken to process the actual theory parts and {\ML} files
   separately.
   
diff -r b38bc78d9a9d -r 66c941ea1f01 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Mon May 03 18:35:48 1999 +0200
+++ b/doc-src/Ref/ref.ind	Mon May 03 19:03:35 1999 +0200
@@ -13,6 +13,7 @@
   \item {\tt\at Finset} constant, 94, 95
   \item {\tt [} symbol, 71
   \item {\tt [|} symbol, 71
+  \item {\tt \$ISABELLE_HOME}, 3
   \item {\tt ]} symbol, 71
   \item {\tt _K} constant, 96, 98
   \item \verb'{}' symbol, 94
@@ -207,7 +208,7 @@
   \item {\tt defer_tac}, \bold{24}
   \item definitions, \see{rewriting, meta-level}{1}, 24, \bold{58}
     \subitem unfolding, 9, 10
-  \item {\tt del_path}, \bold{59}
+  \item {\tt del_path}, \bold{60}
   \item {\tt Delcongs}, \bold{107}
   \item {\tt delcongs}, \bold{112}
   \item {\tt deleqcongs}, \bold{112}
diff -r b38bc78d9a9d -r 66c941ea1f01 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Mon May 03 18:35:48 1999 +0200
+++ b/doc-src/Ref/simplifier.tex	Mon May 03 19:03:35 1999 +0200
@@ -1238,12 +1238,13 @@
 first-order logic; the code is largely taken from {\tt
   FOL/simpdata.ML} of the Isabelle sources.
 
-The simplifier and the case splitting tactic, which reside on separate
-files, are not part of Pure Isabelle.  They must be loaded explicitly
-by the object-logic as follows:
+The simplifier and the case splitting tactic, which reside on separate files,
+are not part of Pure Isabelle.  They must be loaded explicitly by the
+object-logic as follows (below \texttt{\~\relax\~\relax} refers to
+\texttt{\$ISABELLE_HOME}):
 \begin{ttbox}
-use "$ISABELLE_HOME/src/Provers/simplifier.ML";
-use "$ISABELLE_HOME/src/Provers/splitter.ML";
+use "\~\relax\~\relax/src/Provers/simplifier.ML";
+use "\~\relax\~\relax/src/Provers/splitter.ML";
 \end{ttbox}
 
 Simplification requires converting object-equalities to meta-level rewrite
diff -r b38bc78d9a9d -r 66c941ea1f01 doc-src/Ref/tctical.tex
--- a/doc-src/Ref/tctical.tex	Mon May 03 18:35:48 1999 +0200
+++ b/doc-src/Ref/tctical.tex	Mon May 03 19:03:35 1999 +0200
@@ -294,11 +294,10 @@
 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 
 be given to the searching tacticals.
 
-\item[\ttindexbold{eq_thm} ($thm_1$, $thm_2$)] reports whether $thm_1$
-  and $thm_2$ are equal.  Both theorems must have identical
-  signatures.  Both theorems must have the same conclusions, and the
-  same hypotheses, in the same order.  Names of bound variables are
-  ignored.
+\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
+  $thm@2$ are equal.  Both theorems must have identical signatures.  Both
+  theorems must have the same conclusions, and the same hypotheses, in the
+  same order.  Names of bound variables are ignored.
 
 \item[\ttindexbold{size_of_thm} $thm$] 
 computes the size of $thm$, namely the number of variables, constants and
diff -r b38bc78d9a9d -r 66c941ea1f01 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon May 03 18:35:48 1999 +0200
+++ b/doc-src/Ref/theories.tex	Mon May 03 19:03:35 1999 +0200
@@ -243,16 +243,16 @@
 \end{ttbox}
 
 \begin{ttdescription}
-\item[\ttindexbold{use_thy_only} $name$;] is similar to \texttt{use_thy}, but
-  processes the actual theory file $name$\texttt{.thy} only, ignoring
+\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},
+  but processes the actual theory file $name$\texttt{.thy} only, ignoring
   $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand
   from the very beginning, starting with the fresh theory.
   
-\item[\ttindexbold{update_thy} $name$;] is similar to \texttt{use_thy}, but
+\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
   ensures that theory $name$ is fully up-to-date with respect to the file
   system --- apart from $name$ itself its parents may be reloaded as well.
   
-\item[\ttindexbold{touch_thy} $name$;] marks theory node $name$ of the
+\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
   internal graph as outdated.  While the theory remains usable, subsequent
   operations such as \texttt{use_thy} may cause a reload.
   
@@ -281,10 +281,10 @@
 \item[\ttindexbold{show_path}();] displays the load path components in
   canonical string representation, which is always according to Unix rules.
   
-\item[\ttindexbold{add_path} $dir$;] adds component $dir$ to the beginning of
-  the load path.
+\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
+  of the load path.
   
-\item[\ttindexbold{del_path} $dir$;] removes any occurrences of component
+\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
   $dir$ from the load path.
   
 \item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
@@ -292,7 +292,7 @@
 \end{ttdescription}
 
 In operations referring indirectly to some file, such as
-\texttt{use_thy}~$name$, the argument may be prefixed by some directory that
+\texttt{use_thy~"$name$"}, the argument may be prefixed by some directory that
 will be used as temporary load path.  Note that, depending on which parts of
 the ancestry of $name$ are already loaded, the dynamic change of paths might
 be hard to predict.  Use this feature with care only.