# HG changeset patch
# User wenzelm
# Date 881343896 -3600
# Node ID 245b64afefe2e24fb22c2f23e6986fee265332a7
# Parent  2f831a45d5712efa698c5c8282fe2c09b87d0a22
tuned;

diff -r 2f831a45d571 -r 245b64afefe2 doc-src/Ref/goals.tex
--- 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}).
diff -r 2f831a45d571 -r 245b64afefe2 doc-src/Ref/substitution.tex
--- 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
diff -r 2f831a45d571 -r 245b64afefe2 doc-src/Ref/theories.tex
--- 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.