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)}