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