--- 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 \\