| changeset 9695 | ec7d7f877712 |
| parent 9524 | 5721615da108 |
| child 20975 | 5bfa2e4ed789 |
--- a/doc-src/Ref/substitution.tex Mon Aug 28 13:50:24 2000 +0200 +++ b/doc-src/Ref/substitution.tex Mon Aug 28 13:52:38 2000 +0200 @@ -61,7 +61,7 @@ eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.} \end{ttbox} -Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by +Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by \begin{ttbox} fun stac eqth = CHANGED o rtac (eqth RS ssubst); \end{ttbox}