summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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