diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Oct 06 12:31:53 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Oct 06 14:19:48 2000 +0200
@@ -238,7 +238,7 @@
   \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
   \quad \BG \\
   \qquad \FIX{thesis} \\
-  \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
+  \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
   \quad \EN \\
   \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\