1.1 --- a/doc-src/Ref/goals.tex Mon May 03 18:35:48 1999 +0200
1.2 +++ b/doc-src/Ref/goals.tex Mon May 03 19:03:35 1999 +0200
1.3 @@ -309,7 +309,7 @@
1.4 \end{ttdescription}
1.5
1.6 \goodbreak
1.7 -\noindent{\it Error indications for \texttt{back}:}\par\nobreak
1.8 +\noindent{\it Error indications for {\tt back}:}\par\nobreak
1.9 \begin{itemize}
1.10 \item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
1.11 means \texttt{back} found a non-empty branch point, but that it contained
2.1 --- a/doc-src/Ref/introduction.tex Mon May 03 18:35:48 1999 +0200
2.2 +++ b/doc-src/Ref/introduction.tex Mon May 03 19:03:35 1999 +0200
2.3 @@ -145,7 +145,7 @@
2.4 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
2.5 expanded appropriately. Note that \texttt{\~\relax} abbreviates
2.6 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
2.7 -\texttt{\$ISABELLE_HOME}.
2.8 +\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.
2.9
2.10
2.11 \section{Reading theories}\label{sec:intro-theories}
2.12 @@ -177,16 +177,16 @@
2.13 \item[\ttindexbold{the_context}();] obtains the current theory context, or
2.14 raises an error if absent.
2.15
2.16 -\item[\ttindexbold{theory} $name$;] retrieves the theory called $name$ from
2.17 +\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
2.18 the internal database of loaded theories, raising an error if absent.
2.19
2.20 -\item[\ttindexbold{use_thy} $name$;] reads theory $name$ from the file system,
2.21 - looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML}; also
2.22 - makes sure that all parent theories are loaded as well. In case some older
2.23 - versions have already been present, \texttt{use_thy} only tries to reload
2.24 - $name$ itself, but is content with any version of its parents.
2.25 +\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
2.26 + system, looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML};
2.27 + also makes sure that all parent theories are loaded as well. In case some
2.28 + older versions have already been present, \texttt{use_thy} only tries to
2.29 + reload $name$ itself, but is content with any version of its parents.
2.30
2.31 -\item[\ttindexbold{time_use_thy} $name$;] same as \texttt{use_thy}, but
2.32 +\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
2.33 reports the time taken to process the actual theory parts and {\ML} files
2.34 separately.
2.35
3.1 --- a/doc-src/Ref/ref.ind Mon May 03 18:35:48 1999 +0200
3.2 +++ b/doc-src/Ref/ref.ind Mon May 03 19:03:35 1999 +0200
3.3 @@ -13,6 +13,7 @@
3.4 \item {\tt\at Finset} constant, 94, 95
3.5 \item {\tt [} symbol, 71
3.6 \item {\tt [|} symbol, 71
3.7 + \item {\tt \$ISABELLE_HOME}, 3
3.8 \item {\tt ]} symbol, 71
3.9 \item {\tt _K} constant, 96, 98
3.10 \item \verb'{}' symbol, 94
3.11 @@ -207,7 +208,7 @@
3.12 \item {\tt defer_tac}, \bold{24}
3.13 \item definitions, \see{rewriting, meta-level}{1}, 24, \bold{58}
3.14 \subitem unfolding, 9, 10
3.15 - \item {\tt del_path}, \bold{59}
3.16 + \item {\tt del_path}, \bold{60}
3.17 \item {\tt Delcongs}, \bold{107}
3.18 \item {\tt delcongs}, \bold{112}
3.19 \item {\tt deleqcongs}, \bold{112}
4.1 --- a/doc-src/Ref/simplifier.tex Mon May 03 18:35:48 1999 +0200
4.2 +++ b/doc-src/Ref/simplifier.tex Mon May 03 19:03:35 1999 +0200
4.3 @@ -1238,12 +1238,13 @@
4.4 first-order logic; the code is largely taken from {\tt
4.5 FOL/simpdata.ML} of the Isabelle sources.
4.6
4.7 -The simplifier and the case splitting tactic, which reside on separate
4.8 -files, are not part of Pure Isabelle. They must be loaded explicitly
4.9 -by the object-logic as follows:
4.10 +The simplifier and the case splitting tactic, which reside on separate files,
4.11 +are not part of Pure Isabelle. They must be loaded explicitly by the
4.12 +object-logic as follows (below \texttt{\~\relax\~\relax} refers to
4.13 +\texttt{\$ISABELLE_HOME}):
4.14 \begin{ttbox}
4.15 -use "$ISABELLE_HOME/src/Provers/simplifier.ML";
4.16 -use "$ISABELLE_HOME/src/Provers/splitter.ML";
4.17 +use "\~\relax\~\relax/src/Provers/simplifier.ML";
4.18 +use "\~\relax\~\relax/src/Provers/splitter.ML";
4.19 \end{ttbox}
4.20
4.21 Simplification requires converting object-equalities to meta-level rewrite
5.1 --- a/doc-src/Ref/tctical.tex Mon May 03 18:35:48 1999 +0200
5.2 +++ b/doc-src/Ref/tctical.tex Mon May 03 19:03:35 1999 +0200
5.3 @@ -294,11 +294,10 @@
5.4 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may
5.5 be given to the searching tacticals.
5.6
5.7 -\item[\ttindexbold{eq_thm} ($thm_1$, $thm_2$)] reports whether $thm_1$
5.8 - and $thm_2$ are equal. Both theorems must have identical
5.9 - signatures. Both theorems must have the same conclusions, and the
5.10 - same hypotheses, in the same order. Names of bound variables are
5.11 - ignored.
5.12 +\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
5.13 + $thm@2$ are equal. Both theorems must have identical signatures. Both
5.14 + theorems must have the same conclusions, and the same hypotheses, in the
5.15 + same order. Names of bound variables are ignored.
5.16
5.17 \item[\ttindexbold{size_of_thm} $thm$]
5.18 computes the size of $thm$, namely the number of variables, constants and
6.1 --- a/doc-src/Ref/theories.tex Mon May 03 18:35:48 1999 +0200
6.2 +++ b/doc-src/Ref/theories.tex Mon May 03 19:03:35 1999 +0200
6.3 @@ -243,16 +243,16 @@
6.4 \end{ttbox}
6.5
6.6 \begin{ttdescription}
6.7 -\item[\ttindexbold{use_thy_only} $name$;] is similar to \texttt{use_thy}, but
6.8 - processes the actual theory file $name$\texttt{.thy} only, ignoring
6.9 +\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},
6.10 + but processes the actual theory file $name$\texttt{.thy} only, ignoring
6.11 $name$\texttt{.ML}. This might be useful in replaying proof scripts by hand
6.12 from the very beginning, starting with the fresh theory.
6.13
6.14 -\item[\ttindexbold{update_thy} $name$;] is similar to \texttt{use_thy}, but
6.15 +\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
6.16 ensures that theory $name$ is fully up-to-date with respect to the file
6.17 system --- apart from $name$ itself its parents may be reloaded as well.
6.18
6.19 -\item[\ttindexbold{touch_thy} $name$;] marks theory node $name$ of the
6.20 +\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
6.21 internal graph as outdated. While the theory remains usable, subsequent
6.22 operations such as \texttt{use_thy} may cause a reload.
6.23
6.24 @@ -281,10 +281,10 @@
6.25 \item[\ttindexbold{show_path}();] displays the load path components in
6.26 canonical string representation, which is always according to Unix rules.
6.27
6.28 -\item[\ttindexbold{add_path} $dir$;] adds component $dir$ to the beginning of
6.29 - the load path.
6.30 +\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
6.31 + of the load path.
6.32
6.33 -\item[\ttindexbold{del_path} $dir$;] removes any occurrences of component
6.34 +\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
6.35 $dir$ from the load path.
6.36
6.37 \item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
6.38 @@ -292,7 +292,7 @@
6.39 \end{ttdescription}
6.40
6.41 In operations referring indirectly to some file, such as
6.42 -\texttt{use_thy}~$name$, the argument may be prefixed by some directory that
6.43 +\texttt{use_thy~"$name$"}, the argument may be prefixed by some directory that
6.44 will be used as temporary load path. Note that, depending on which parts of
6.45 the ancestry of $name$ are already loaded, the dynamic change of paths might
6.46 be hard to predict. Use this feature with care only.