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