author wenzelm Fri, 05 Dec 1997 18:44:56 +0100 changeset 4374 245b64afefe2 parent 4373 2f831a45d571 child 4375 ef2a7b589004
tuned;
 doc-src/Ref/goals.tex file | annotate | diff | comparison | revisions doc-src/Ref/substitution.tex file | annotate | diff | comparison | revisions doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- 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.