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