--- 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