changeset 58249 | 180f1b3508ed |
parent 51717 | 9e7d1c139569 |
child 58310 | 91ea607a34d8 |
58248:25af24e1f37b | 58249:180f1b3508ed |
---|---|
164 where "incX' r = r (| xpos := xpos r + 1 |)" |
164 where "incX' r = r (| xpos := xpos r + 1 |)" |
165 |
165 |
166 |
166 |
167 subsection {* Coloured points: record extension *} |
167 subsection {* Coloured points: record extension *} |
168 |
168 |
169 datatype colour = Red | Green | Blue |
169 datatype_new colour = Red | Green | Blue |
170 |
170 |
171 record cpoint = point + |
171 record cpoint = point + |
172 colour :: colour |
172 colour :: colour |
173 |
173 |
174 |
174 |