equal
deleted
inserted
replaced
19 *) |
19 *) |
20 |
20 |
21 Buffer = FOCUS + |
21 Buffer = FOCUS + |
22 |
22 |
23 types D |
23 types D |
24 arities D::term |
24 arities D :: type |
25 |
25 |
26 datatype |
26 datatype |
27 |
27 |
28 M = Md D | Mreq ("\\<bullet>") |
28 M = Md D | Mreq ("\\<bullet>") |
29 |
29 |