| changeset 164 | 3f617d7a2691 |
| parent 162 | 3fb9f820a294 |
| child 168 | 009ca4807baa |
| 163:2319cff107f0 | 164:3f617d7a2691 |
|---|---|
16 @{ML "ProofContext.print_syntax"} |
16 @{ML "ProofContext.print_syntax"} |
17 |
17 |
18 user space type systems (in the form that already exists) |
18 user space type systems (in the form that already exists) |
19 |
19 |
20 unification and typing algorithms |
20 unification and typing algorithms |
21 |
|
22 useful datastructures: |
|
23 |
|
24 discrimination nets |
|
25 |
|
26 association lists |
|
21 *} |
27 *} |
22 |
28 |
23 end |
29 end |
24 |
30 |
25 |
31 |