--- a/doc-src/IsarRef/generic.tex Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Jul 30 18:27:25 1999 +0200
@@ -28,8 +28,8 @@
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
c@2$] setup up a goal stating the class relation or type arity. The proof
would usually proceed by the $expand_classes$ method, and then establish the
- characteristic theorems of the type classes involved. After the final
- $\QED{}$, the theory will be augmented by a type signature declaration
+ characteristic theorems of the type classes involved. After finishing the
+ proof the theory will be augmented by a type signature declaration
corresponding to the resulting theorem.
\end{description}