| changeset 5371 | e27558a68b8d |
| parent 4596 | 0c32a609fcad |
| child 6618 | 13293a7d4a57 |
--- a/doc-src/Ref/substitution.tex Mon Aug 24 19:11:13 1998 +0200 +++ b/doc-src/Ref/substitution.tex Mon Aug 24 19:12:13 1998 +0200 @@ -206,3 +206,9 @@ by calling \hbox{\tt resolve_tac\ts[imp_intr]}. \index{equality|)}\index{tactics!substitution|)} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "ref" +%%% End: