--- a/doc-src/Ref/goals.tex Fri Dec 05 17:31:01 1997 +0100
+++ b/doc-src/Ref/goals.tex Fri Dec 05 18:44:56 1997 +0100
@@ -157,7 +157,7 @@
\ttindex{assume_ax} has been used.
\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
- stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
+ stores {\tt standard $thm$} (see \S\ref{MiscellaneousForwardRules})
in the theorem database associated with its theory and in the {\ML}
variable $name$. The theorem can be retrieved from the database
using {\tt get_thm} (see \S\ref{BasicOperationsOnTheories}).
--- a/doc-src/Ref/substitution.tex Fri Dec 05 17:31:01 1997 +0100
+++ b/doc-src/Ref/substitution.tex Fri Dec 05 18:44:56 1997 +0100
@@ -78,7 +78,7 @@
assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can
work out a solution. First apply {\tt eresolve_tac\ts[subst]\ts\(i\)},
replacing~$a$ by~$c$:
-\[ \List{c=b} \Imp c=b \]
+\[ c=b \Imp c=b \]
Equality reasoning can be difficult, but this trivial proof requires
nothing more sophisticated than substitution in the assumptions.
Object-logics that include the rule~$(subst)$ provide tactics for this
--- a/doc-src/Ref/theories.tex Fri Dec 05 17:31:01 1997 +0100
+++ b/doc-src/Ref/theories.tex Fri Dec 05 18:44:56 1997 +0100
@@ -588,7 +588,7 @@
incr_boundvars : int -> term -> term
abstract_over : term*term -> term
variant_abs : string * typ * term -> string * term
-aconv : term*term -> bool\hfill{\bf infix}
+aconv : term * term -> bool\hfill{\bf infix}
\end{ttbox}
These functions are all concerned with the de Bruijn representation of
bound variables.