changeset 41778 | 5f79a9e42507 |
parent 38540 | 8c08631cb4b6 |
child 45471 | 489f27dcc0f4 |
41777:1f7cbe39d425 | 41778:5f79a9e42507 |
---|---|
1399 qed |
1399 qed |
1400 |
1400 |
1401 section "fields and methods" |
1401 section "fields and methods" |
1402 |
1402 |
1403 |
1403 |
1404 types |
1404 type_synonym |
1405 fspec = "vname \<times> qtname" |
1405 fspec = "vname \<times> qtname" |
1406 |
1406 |
1407 translations |
1407 translations |
1408 (type) "fspec" <= (type) "vname \<times> qtname" |
1408 (type) "fspec" <= (type) "vname \<times> qtname" |
1409 |
1409 |