doc-src/IsarRef/generic.tex
 changeset 7141 a67dde8820c0 parent 7135 8eabfd7e6b9b child 7167 0b2e3ef1d8f4
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Jul 30 15:59:00 1999 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Jul 30 18:27:25 1999 +0200
1.3 @@ -28,8 +28,8 @@
1.4  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 < 1.5 c@2$] setup up a goal stating the class relation or type arity.  The proof
1.6    would usually proceed by the $expand_classes$ method, and then establish the
1.7 -  characteristic theorems of the type classes involved.  After the final
1.8 -  $\QED{}$, the theory will be augmented by a type signature declaration
1.9 +  characteristic theorems of the type classes involved.  After finishing the
1.10 +  proof the theory will be augmented by a type signature declaration
1.11    corresponding to the resulting theorem.
1.12  \end{description}
1.13