1.1 --- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Thu Sep 29 09:37:59 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Mon Oct 03 11:14:19 2011 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  \begin{isamarkuptext}%
     1.5  \noindent Substitution is very powerful, but also hard to control in
     1.6    full generality.  We derive some common symmetry~/ transitivity
     1.7 -  schemes of as particular consequences.%
     1.8 +  schemes of \isa{equal} as particular consequences.%
     1.9  \end{isamarkuptext}%
    1.10  \isamarkuptrue%
    1.11  \isacommand{theorem}\isamarkupfalse%