doc-src/Ref/simplifier.tex
changeset 6569 66c941ea1f01
parent 5776 3bcc29d0c783
child 7620 8d721c3f4acb
--- 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