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