equal
deleted
inserted
replaced
26 \begin{description} |
26 \begin{description} |
27 \item [$\isarkeyword{axclass}~$] FIXME |
27 \item [$\isarkeyword{axclass}~$] FIXME |
28 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 < |
28 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 < |
29 c@2$] setup up a goal stating the class relation or type arity. The proof |
29 c@2$] setup up a goal stating the class relation or type arity. The proof |
30 would usually proceed by the $expand_classes$ method, and then establish the |
30 would usually proceed by the $expand_classes$ method, and then establish the |
31 characteristic theorems of the type classes involved. After the final |
31 characteristic theorems of the type classes involved. After finishing the |
32 $\QED{}$, the theory will be augmented by a type signature declaration |
32 proof the theory will be augmented by a type signature declaration |
33 corresponding to the resulting theorem. |
33 corresponding to the resulting theorem. |
34 \end{description} |
34 \end{description} |
35 |
35 |
36 |
36 |
37 |
37 |