diff -r d7e85fd09291 -r 3fc32155372c doc-src/ZF/FOL.tex
--- a/doc-src/ZF/FOL.tex	Wed Feb 16 10:50:57 2000 +0100
+++ b/doc-src/ZF/FOL.tex	Wed Feb 16 10:51:23 2000 +0100
@@ -578,12 +578,12 @@
 {\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
 \end{ttbox}
 In classical logic, a negated assumption is equivalent to a conclusion.  To
-get this effect, we create a swapped version of~$(\forall I)$ and apply it
-using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall
+get this effect, we create a swapped version of $(\forall I)$ and apply it
+using \ttindex{eresolve_tac}; we could equivalently have applied $(\forall
 I)$ using \ttindex{swap_res_tac}.
 \begin{ttbox}
 allI RSN (2,swap);
-{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
+{\out val it = "[| ~(ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
 by (eresolve_tac [it] 1);
 {\out Level 5}
 {\out EX y. ALL x. P(y) --> P(x)}