| changeset 58249 | 180f1b3508ed |
| parent 45827 | 66c68453455c |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
34 } |
34 } |
35 } |
35 } |
36 \end{verbatim} |
36 \end{verbatim} |
37 *} |
37 *} |
38 |
38 |
39 datatype cnam' = Base' | Ext' |
39 datatype_new cnam' = Base' | Ext' |
40 datatype vnam' = vee' | x' | e' |
40 datatype_new vnam' = vee' | x' | e' |
41 |
41 |
42 text {* |
42 text {* |
43 @{text cnam'} and @{text vnam'} are intended to be isomorphic |
43 @{text cnam'} and @{text vnam'} are intended to be isomorphic |
44 to @{text cnam} and @{text vnam} |
44 to @{text cnam} and @{text vnam} |
45 *} |
45 *} |